transcript: we now check for non-existing objects

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

diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma
index eff18dbae153ffe239c98129926dbe2ee3b23310..5d99d3db502f8f8ba00a945d017d6700a817686f 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma
@@ -16,9 +16,9 @@
 
 include "Coq.ma".
 
-(*s Definition of inequality *)
-
 include "Num/Params.ma".
 
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/NeqDef/neq.con ********************)
+
 inline procedural "cic:/Coq/Num/Nat/NeqDef/neq.con" as definition.