transcript: we now check for non-existing objects

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

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 c2b48712201adbb9c77ac1d8dd26c9deb9804c0c..ccc8303b40104bb51e8d346537c05c324b581dbe 100644 (file)
--- 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 ] ]
-.
-*)
-