auto ==> autobatch

[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..1bf18389f3c5ba30915965fbd52aa9e565250829 100644 (file)
--- a/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
@@ -17,9 +17,8 @@ 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)
 .
+*)