From 0cb045e7fe606a61ff725a2408684bb390bcb50c Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 5 Sep 2003 16:18:53 +0000
Subject: [PATCH] added notation for Ropp and Rinv

---
 .../cic_transformations/cexpr2pres_hashtbl.ml | 21 +++++++++++++++++++
 .../content_expressions.ml                    | 16 ++++++++++++++
 2 files changed, 37 insertions(+)

diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
index 676b55dc4..79c9943c9 100644
--- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
+++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
@@ -214,6 +214,27 @@ Hashtbl.add C2P.symbol_table "not" (unary
        P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
        cexpr2pres a;P.Mtext([],")")])));
 
+(* inv *)
+Hashtbl.add C2P.symbol_table "inv" (unary
+  (fun a ~priority ~assoc ~tail attr sattr ->
+    P.Msup([],
+      P.Mrow([],[
+        P.Mtext([],"(");
+        cexpr2pres a;
+        P.Mtext([],")")]),
+      P.Mrow([],[
+        P.Mo([],"-");
+        P.Mn([],"1")]))));
+
+(* opp *)
+Hashtbl.add C2P.symbol_table "opp" (unary
+  (fun a ~priority ~assoc ~tail attr sattr ->
+    P.Mrow([],[
+      P.Mo([],"-");
+      P.Mtext([],"(");
+      cexpr2pres a;
+      P.Mtext([],")")])));
+
 (* leq *)
 Hashtbl.add C2P.symbol_table "leq" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
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 ->
-- 
2.39.2