transcript: we now check for non-existing objects

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

diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Params.mma b/helm/software/matita/contribs/procedural/Coq/Num/Params.mma
index e076c3aebadd858bd0943ff8414d125d71af47d5..003da89e6d4a01741583876e7e7de9f6fe11a421 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Num/Params.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Num/Params.mma
@@ -16,48 +16,39 @@
 
 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       *)
-
-(*#**********************************************************************)
-
-(*i $Id: Params.v,v 1.2 2002/02/14 14:39:04 filliatr Exp $ i*)
-
-(*#* 
-  Axiomatisation of a numerical set 
-
-  It will be instantiated by Z and R later on
-  We choose to introduce many operation to allow flexibility in definition 
-  ([S] is primitive in the definition of [nat] while [add] and [one] 
-   are primitive in the definition 
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/N.con **************************)
 
 inline procedural "cic:/Coq/Num/Params/N.con".
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/zero.con ***********************)
+
 inline procedural "cic:/Coq/Num/Params/zero.con".
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/one.con ************************)
+
 inline procedural "cic:/Coq/Num/Params/one.con".
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/add.con ************************)
+
 inline procedural "cic:/Coq/Num/Params/add.con".
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/S.con **************************)
+
 inline procedural "cic:/Coq/Num/Params/S.con".
 
-(*#* Relations, equality is defined separately *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/lt.con *************************)
 
 inline procedural "cic:/Coq/Num/Params/lt.con".
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/le.con *************************)
+
 inline procedural "cic:/Coq/Num/Params/le.con".
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/gt.con *************************)
+
 inline procedural "cic:/Coq/Num/Params/gt.con".
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/ge.con *************************)
+
 inline procedural "cic:/Coq/Num/Params/ge.con".