+ | expr2 RPLUS expr2
+ { let dom1,mk_expr1 = $1 in
+ let dom2,mk_expr2 = $3 in
+ let dom = union dom1 dom2 in
+ dom, function interp ->
+ Cic.Appl
+ [Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
+ (mk_expr1 interp) ;
+ (mk_expr2 interp)
+ ]
+ }
+ | expr2 RMINUS expr2
+ { let dom1,mk_expr1 = $1 in
+ let dom2,mk_expr2 = $3 in
+ let dom = union dom1 dom2 in
+ dom, function interp ->
+ Cic.Appl
+ [Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rminus.con",[]) ;
+ (mk_expr1 interp) ;
+ (mk_expr2 interp)
+ ]
+ }
+ | expr2 RTIMES expr2
+ { let dom1,mk_expr1 = $1 in
+ let dom2,mk_expr2 = $3 in
+ let dom = union dom1 dom2 in
+ dom, function interp ->
+ Cic.Appl
+ [Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rmult.con",[]) ;
+ (mk_expr1 interp) ;
+ (mk_expr2 interp)
+ ]
+ }
+ | expr2 RDIV expr2
+ { let dom1,mk_expr1 = $1 in
+ let dom2,mk_expr2 = $3 in
+ let dom = union dom1 dom2 in
+ dom, function interp ->
+ Cic.Appl
+ [Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rdiv.con",[]) ;
+ (mk_expr1 interp) ;
+ (mk_expr2 interp)
+ ]
+ }