X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FNum%2FNat%2FNSyntax.mma;h=ccc8303b40104bb51e8d346537c05c324b581dbe;hb=f620bf94af6c347926ed1c2328462efab7018b21;hp=c2b48712201adbb9c77ac1d8dd26c9deb9804c0c;hpb=418b1f26ab67b824c79d1146fdb50ca29b34c1f6;p=helm.git

diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma
index c2b487122..ccc8303b4 100644
--- a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma
@@ -16,44 +16,3 @@
 
 include "Coq.ma".
 
-(*s Syntax for arithmetic *)
-
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(*i Infix 7 "+" plus. i*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
-  squash_sum
-  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
-      case [$c2] of
-        (SQUASH $T2) ->
-            case [$c1] of
-              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
-            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
-            esac
-      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
-      esac.
-*)
-
-(* NOTATION
-Syntax constr
-  level 4:
-    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-