X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FNum%2FLeProps.mma;h=83e33fc152efb5f6847ef6247688d5c6ffd7100e;hb=f620bf94af6c347926ed1c2328462efab7018b21;hp=8493c65861ab0deeb80c7d3fb09f923986bc051c;hpb=418b1f26ab67b824c79d1146fdb50ca29b34c1f6;p=helm.git

diff --git a/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma
index 8493c6586..83e33fc15 100644
--- a/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma
@@ -16,115 +16,67 @@
 
 include "Coq.ma".
 
-(*#**********************************************************************)
-
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-
-(*   \VV/  *************************************************************)
-
-(*    //   *      This file is distributed under the terms of the      *)
-
-(*         *       GNU Lesser General Public License Version 2.1       *)
-
-(*#**********************************************************************)
-
 include "Num/LtProps.ma".
 
 include "Num/LeAxioms.ma".
 
-(*#* Properties of the relation [<=] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_le.con *********************)
 
 inline procedural "cic:/Coq/Num/LeProps/lt_le.con" as lemma.
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/eq_le.con *********************)
+
 inline procedural "cic:/Coq/Num/LeProps/eq_le.con" as lemma.
 
-(*#* compatibility with equality *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_eq_compat.con **************)
 
 inline procedural "cic:/Coq/Num/LeProps/le_eq_compat.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve le_eq_compat : num.
-*)
-
-(*#* Transitivity *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_trans.con ******************)
 
 inline procedural "cic:/Coq/Num/LeProps/le_trans.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve le_trans : num.
-*)
-
-(*#* compatibility with equality, addition and successor *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat_l.con ***********)
 
 inline procedural "cic:/Coq/Num/LeProps/le_add_compat_l.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve le_add_compat_l : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat_r.con ***********)
 
 inline procedural "cic:/Coq/Num/LeProps/le_add_compat_r.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve le_add_compat_r : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat.con *************)
 
 inline procedural "cic:/Coq/Num/LeProps/le_add_compat.con" as lemma.
 
-(* UNEXPORTED
-Hints Immediate le_add_compat : num.
-*)
-
-(* compatibility with successor *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_S_compat.con ***************)
 
 inline procedural "cic:/Coq/Num/LeProps/le_S_compat.con" as lemma.
 
-(* UNEXPORTED
-Hints Resolve le_S_compat : num.
-*)
-
-(*#* relating [<=] with [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_lt_x_Sy.con ****************)
 
 inline procedural "cic:/Coq/Num/LeProps/le_lt_x_Sy.con" as lemma.
 
-(* UNEXPORTED
-Hints Immediate le_lt_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_le_x_Sy.con ****************)
 
 inline procedural "cic:/Coq/Num/LeProps/le_le_x_Sy.con" as lemma.
 
-(* UNEXPORTED
-Hints Immediate le_le_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_Sx_y_lt.con ****************)
 
 inline procedural "cic:/Coq/Num/LeProps/le_Sx_y_lt.con" as lemma.
 
-(* UNEXPORTED
-Hints Immediate le_Sx_y_lt : num.
-*)
-
-(*#* Combined transitivity *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_le_trans.con ***************)
 
 inline procedural "cic:/Coq/Num/LeProps/lt_le_trans.con" as lemma.
 
-inline procedural "cic:/Coq/Num/LeProps/le_lt_trans.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_lt_trans.con ***************)
 
-(* UNEXPORTED
-Hints Immediate lt_le_trans le_lt_trans : num.
-*)
+inline procedural "cic:/Coq/Num/LeProps/le_lt_trans.con" as lemma.
 
-(*#* weaker compatibility results involving [<] and [<=] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_add_compat_weak_l.con ******)
 
 inline procedural "cic:/Coq/Num/LeProps/lt_add_compat_weak_l.con" as lemma.
 
-(* UNEXPORTED
-Hints Immediate  lt_add_compat_weak_l : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_add_compat_weak_r.con ******)
 
 inline procedural "cic:/Coq/Num/LeProps/lt_add_compat_weak_r.con" as lemma.
 
-(* UNEXPORTED
-Hints Immediate lt_add_compat_weak_r : num.
-*)
-