Notation for Rdiv and Rminus.

[helm.git] / helm / ocaml / cic_transformations / content_expressions.ml

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 717b4e925b50eb55c2c88d551b73f7385a5ac3a3..22f959927335208c2a9bf45c73c8fe7819a11d29 100644 (file)
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -235,6 +235,21 @@ Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con"
           None, Some "cic:/Coq/Arith/Minus/mult.con"))
      :: List.map acic2cexpr args));;
 
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con" 
+  (fun aid sid args acic2cexpr ->
+   Appl 
+    (Some aid, (Symbol (Some sid, "minus",
+          None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
+     :: List.map acic2cexpr args));;
+
+(* div *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" 
+  (fun aid sid args acic2cexpr ->
+   Appl 
+    (Some aid, (Symbol (Some sid, "div",
+          None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
+     :: List.map acic2cexpr args));;
+