Horrible workaround

[helm.git] / helm / software / matita / contribs / LOGIC / NTrack / defs.ma

diff --git a/helm/software/matita/contribs/LOGIC/NTrack/defs.ma b/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
index b04cf4bd1af0ba51f3dc62a54e4b87c0f3582d99..15560f19c1417607fab0cf3b30d4ca9159a9f573 100644 (file)
--- a/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
@@ -12,14 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/NTrack/defs".
+
 
 (* NORMAL PROOF TREE TRACKS
 *)
 
-include "datatypes/Proof.ma".
 include "Insert/defs.ma".
-
+(*
 inductive NTrack: Context \to Proof \to Sequent \to Prop \def
    | ntrack_proj: \forall P,Q,S,i. Insert S i P Q \to NTrack Q (lref i) S
    | ntrack_posr: \forall P,h.
@@ -36,3 +35,4 @@ inductive NTrack: Context \to Proof \to Sequent \to Prop \def
                  Insert (pair A B) i P Q \to
                  NTrack P (impi p q r) (pair (impl a b) D)
 .
+*)