X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=52318d1c010d7e25818c8a4b6d6180e995e1fe54;hb=0cb045e7fe606a61ff725a2408684bb390bcb50c;hp=22f959927335208c2a9bf45c73c8fe7819a11d29;hpb=48d41935cc96e8898cc5e3da98a1706294b7b411;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 22f959927..52318d1c0 100644
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -113,6 +113,22 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con"
           None, Some "cic:/Coq/Init/Logic/not.con"))
      :: List.map acic2cexpr args));;
 
+(* Rinv *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con"
+  (fun aid sid args acic2cexpr ->
+   Appl 
+    (Some aid, (Symbol (Some sid, "inv",
+          None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+     :: List.map acic2cexpr args));;
+
+(* Ropp *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+  (fun aid sid args acic2cexpr ->
+   Appl 
+    (Some aid, (Symbol (Some sid, "opp",
+          None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+     :: List.map acic2cexpr args));;
+
 (* exists *)
 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->