transcript: we now check for non-existing objects

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

diff --git a/helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma b/helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma
index ebc29c0cc58fb07f78b619b6fc5c2c0540c66303..feea9e6882ca5d94845e106b8282b900617ca6f2 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma
@@ -16,40 +16,9 @@
 
 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: EqParams.v,v 1.4 2003/03/21 17:37:16 barras Exp $ i*)
-
-(*#* Equality is introduced as an independant parameter, it could be 
-    instantiated with Leibniz equality *)
-
 include "Num/Params.ma".
 
-inline procedural "cic:/Coq/Num/EqParams/eqN.con".
-
-(*i Infix 6 "=" eqN V8only 50. i*)
-
-(* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqParams/eqN.con **********************)
 
-(* NOTATION
-Syntax constr
-  level 1:
-    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
-.
-*)
+inline procedural "cic:/Coq/Num/EqParams/eqN.con".