transcript: we now check for non-existing objects

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

diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma
index f473e4dc0c61738415de32924f333ad406708839..0693b7d97a921b3c896d60e76056ac72588d2d7a 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma
@@ -16,60 +16,33 @@
 
 include "Coq.ma".
 
-(*s Instantiating [eqN] with Leibniz equality *)
-
 include "Num/NSyntax.ma".
 
-inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eqN.con" as definition.
-
-(* UNEXPORTED
-Hints Unfold eqN : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eqN.con **************)
 
-(* 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 ] ].
-*)
+inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eqN.con" as definition.
 
-(*s Lemmas for [eqN] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_refl.con **********)
 
 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_refl.con" as lemma.
 
-inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con ***********)
 
-inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con" as lemma.
+inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve eq_refl eq_trans : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con *********)
 
-(* UNEXPORTED
-Hints Immediate eq_sym : num.
-*)
+inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con" as lemma.
 
-(*s Compatibility lemmas for [S], [add], [lt] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/S_eq_compat.con ******)
 
 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/S_eq_compat.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve S_eq_compat : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/add_eq_compat.con ****)
 
 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/add_eq_compat.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve add_eq_compat : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/lt_eq_compat.con *****)
 
 inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/lt_eq_compat.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve add_eq_compat S_eq_compat lt_eq_compat : num.
-*)
-