transcript: we now check for non-existing objects

[helm.git] / helm / software / matita / contribs / procedural / Coq / Num / Leibniz / NSyntax.mma

diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma
index b80b0c5926acec49f9e78d159a431c38c4f33048..83b4afc31f0a40b3cda770973b6b27eeb8726940 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma
@@ -16,50 +16,5 @@
 
 include "Coq.ma".
 
-(*s Syntax for arithmetic *)
-
 include "Num/Params.ma".
 
-(* 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 1:
-    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
- ;
-
-  level 4:
-    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-