transcript: we now check for non-existing objects

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

diff --git a/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma
index 8493c65861ab0deeb80c7d3fb09f923986bc051c..83e33fc152efb5f6847ef6247688d5c6ffd7100e 100644 (file)
--- 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.
-*)
-