transcript: we now check for non-existing objects

[helm.git] / helm / software / matita / contribs / procedural / Coq / Coq.ma

diff --git a/helm/software/matita/contribs/procedural/Coq/Coq.ma b/helm/software/matita/contribs/procedural/Coq/Coq.ma
index 8b1c5bd3a84e37ff5043774d3eea109fd2fec9ec..eadacbd53aecac631e3e968b888ccd060858c9ce 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Coq.ma
+++ b/helm/software/matita/contribs/procedural/Coq/Coq.ma
@@ -345,164 +345,40 @@ Infix "::" := cons (at level 60, right associativity) : list_scope.
 Infix "++" := app (right associativity, at level 60) : list_scope.
 *)
 
-(* From Num/Leibniz/EqAxioms **********************************************)
-
-(* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
-*)
-
-(* NOTATION
-Syntax constr
-  level 1:
-    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ].
-*)
-
-(* From Num/Leibniz/NSyntax ***********************************************)
-
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(* 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 ] ]
-.
-*)
-
-(* From Num/Nat/NSyntax ***************************************************)
-
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(* 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 ] ]
-.
-*)
-
-(* From Num/EqParams ******************************************************)
+(* From NArith/BinNat *****************************************************)
 
 (* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
+Infix "+" := Nplus : N_scope.
 *)
 
 (* NOTATION
-Syntax constr
-  level 1:
-    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
-.
-*)
-
-(* From Num/NSyntax *******************************************************)
-
-(* NOTATION
-Infix 6 "<" lt V8only 70.
+Infix "*" := Nmult : N_scope.
 *)
 
 (* NOTATION
-Infix 6 "<=" le V8only 70.
+Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
 *)
 
-(* NOTATION
-Infix 6 ">" gt V8only 70.
-*)
+(* From NArith/BinPos *****************************************************)
 
 (* NOTATION
-Infix 6 ">=" ge V8only 70.
+Infix "+" := Pplus : positive_scope.
 *)
 
 (* 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.
+Infix "-" := Pminus : positive_scope.
 *)
 
 (* NOTATION
-Syntax constr
-  level 4:
-    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
+Infix "*" := Pmult : positive_scope.
 *)
 
-(* From Num/NeqDef ********************************************************)
-
 (* NOTATION
-Infix 6 "<>" neq V8only 70.
+Infix "/" := Pdiv2 : positive_scope.
 *)
 
-(* From Num/NeqParams *****************************************************)
-
 (* NOTATION
-Infix 6 "<>" neq V8only 70.
+Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
 *)
 
 (* From Reals/RIneq *******************************************************)
@@ -635,26 +511,6 @@ Add Setoid Prop iff Prop_S.
 Notation Le_AsB := (le_AsB A B leA leB).
 *)
 
-(* From Wellfounded/Lexicographic_Product *********************************)
-
-(* NOTATION
-Notation LexProd := (lexprod A B leA leB).
-*)
-
-(* NOTATION
-Notation Symprod := (symprod A B leA leB).
-*)
-
-(* NOTATION
-Notation SwapProd := (swapprod A R).
-*)
-
-(* From Wellfounded/Union *************************************************)
-
-(* NOTATION
-Notation Union := (union A R1 R2).
-*)
-
 (* From Wellfounded/Lexicographic_Exponentiation **************************)
 
 (* NOTATION
@@ -689,30 +545,30 @@ Notation Cons := (cons (A:=A)).
 Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
 *)
 
-(* From Wellfounded/Transitive_Closure ************************************)
+(* From Wellfounded/Lexicographic_Product *********************************)
 
 (* NOTATION
-Notation trans_clos := (clos_trans A R).
+Notation LexProd := (lexprod A B leA leB).
 *)
 
-(* From ZArith/Zdiv *******************************************************)
-
 (* NOTATION
-Infix "/" := Zdiv : Z_scope.
+Notation Symprod := (symprod A B leA leB).
 *)
 
 (* NOTATION
-Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
+Notation SwapProd := (swapprod A R).
 *)
 
-(* From ZArith/Zpower *****************************************************)
+(* From Wellfounded/Transitive_Closure ************************************)
 
 (* NOTATION
-Infix "^" := Zpower : Z_scope.
+Notation trans_clos := (clos_trans A R).
 *)
 
+(* From Wellfounded/Union *************************************************)
+
 (* NOTATION
-Infix "^" := Zpower : Z_scope.
+Notation Union := (union A R1 R2).
 *)
 
 (* From ZArith/BinInt *****************************************************)
@@ -769,45 +625,29 @@ Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 *)
 
-(* From ZArith/Znumtheory *************************************************)
-
-(* NOTATION
-Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
-*)
-
-(* From NArith/BinNat *****************************************************)
-
-(* NOTATION
-Infix "+" := Nplus : N_scope.
-*)
+(* From ZArith/Zdiv *******************************************************)
 
 (* NOTATION
-Infix "*" := Nmult : N_scope.
+Infix "/" := Zdiv : Z_scope.
 *)
 
 (* NOTATION
-Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
+Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
 *)
 
-(* From NArith/BinPos *****************************************************)
-
-(* NOTATION
-Infix "+" := Pplus : positive_scope.
-*)
+(* From ZArith/Znumtheory *************************************************)
 
 (* NOTATION
-Infix "-" := Pminus : positive_scope.
+Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
 *)
 
-(* NOTATION
-Infix "*" := Pmult : positive_scope.
-*)
+(* From ZArith/Zpower *****************************************************)
 
 (* NOTATION
-Infix "/" := Pdiv2 : positive_scope.
+Infix "^" := Zpower : Z_scope.
 *)
 
 (* NOTATION
-Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
+Infix "^" := Zpower : Z_scope.
 *)