From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Sep 2003 12:34:07 +0000 (+0000)
Subject: Notation for Rdiv and Rminus.
X-Git-Tag: v0_0_1~35
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4a5311d795b19019a675f60c33710301873f646c

Notation for Rdiv and Rminus.
---

diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
index 657464270..676b55dc4 100644
--- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
+++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
@@ -415,5 +415,34 @@ Hashtbl.add C2P.symbol_table_charcount "minus" (binary
        P.two_rows_table_without_brackets aattr
          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
-         (P.Mo(sattr,"-"))))
+         (P.Mo(sattr,"-"))));
+
+(* div *)
+Hashtbl.add C2P.symbol_table "div" (binary
+  (fun a b ~priority ~assoc ~tail aattr sattr ->
+     if (priority > 60) || (priority = 60 && assoc) then
+       P.row_with_brackets aattr
+         (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
+         (cexpr2pres ~priority:60 ~assoc:false 
+            ~tail:(P.Mtext([],")")::tail) b)
+         (P.Mo(sattr,"/"))
+     else 
+       P.row_without_brackets aattr
+         (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
+         (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
+         (P.Mo(sattr,"/"))));
+
+Hashtbl.add C2P.symbol_table_charcount "div" (binary
+  (fun a b ~priority ~assoc ~tail aattr sattr ->
+     if (priority > 60) || (priority = 60 && assoc) then
+       P.two_rows_table_with_brackets aattr
+         (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
+         (cexpr2pres_charcount ~priority:60 ~assoc:false 
+           ~tail:(P.Mtext([],")")::tail) b)
+         (P.Mo(sattr,"/"))
+     else
+       P.two_rows_table_without_brackets aattr
+         (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
+         (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
+         (P.Mo(sattr,"/"))))
 ;;
diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 717b4e925..22f959927 100644
--- 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));;
+