X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLOGIC%2FNTrack%2Fdefs.ma;h=15560f19c1417607fab0cf3b30d4ca9159a9f573;hb=2c486bbea1d6ffb072d0ff83f9df129b7860f3e1;hp=b04cf4bd1af0ba51f3dc62a54e4b87c0f3582d99;hpb=3784663281673f2549ab856d36441dfd24dcc593;p=helm.git

diff --git a/helm/software/matita/contribs/LOGIC/NTrack/defs.ma b/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
index b04cf4bd1..15560f19c 100644
--- 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)
 .
+*)