X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FNum%2FLeibniz%2FEqAxioms.mma;h=0693b7d97a921b3c896d60e76056ac72588d2d7a;hb=f620bf94af6c347926ed1c2328462efab7018b21;hp=f473e4dc0c61738415de32924f333ad406708839;hpb=29714797b01e0ac8c22e4df2827b1785a759f482;p=helm.git

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 f473e4dc0..0693b7d97 100644
--- 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.
-*)
-