bug fix in Track definition

[helm.git] / matita / contribs / LOGIC / PNF / defs.ma

diff --git a/matita/contribs/LOGIC/PNF/defs.ma b/matita/contribs/LOGIC/PNF/defs.ma
index 12a3b7be8d5ea2c68a7741df735cd5841256d20b..feea35b43b031964ad28d4b575a8c8cb33c9964f 100644 (file)
--- a/matita/contribs/LOGIC/PNF/defs.ma
+++ b/matita/contribs/LOGIC/PNF/defs.ma
@@ -18,7 +18,8 @@ set "baseuri" "cic:/matita/LOGIC/PNF/defs".
 *)
 
 include "PRed/defs.ma".
-
+(*
 inductive PNF: Proof \to Prop \def
    | pnf: \forall p. (\forall q. p => q \to p = q) \to PNF p
 .
+*)