- [Cic.Const
- (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ;
- (mk_expr1 interp) ;
- (mk_expr2 interp)
- ]
- }
- | expr2 EQT expr2
- { let dom1,mk_expr1 = $1 in
- let dom2,mk_expr2 = $3 in
- let dom3,mk_expr3 = mk_implicit () in
- let dom = union dom1 (union dom2 dom3) in
- dom, function interp ->
- Cic.Appl
- [Cic.MutInd
- (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
- (mk_expr3 interp) ;