From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 10 Sep 2008 09:17:16 +0000 (+0000)
Subject: COMMIT TO JUST RUN A BENCH, SHOULD BE REVERTED ASAP (auto run after every tactic)
X-Git-Tag: make_still_working~4794
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6bce12e43e808de17a7146584c40ab26d29498e5;p=helm.git

COMMIT TO JUST RUN A BENCH, SHOULD BE REVERTED ASAP (auto run after every tactic)
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index fd1eb3484..d85110774 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -794,15 +794,17 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
 ~disambiguate_macro opts status (text,prefix_len,ex) ->
   match ex with
-  | GrafiteAst.Tactic (_(*loc*), Some tac, punct) ->
+  | GrafiteAst.Tactic (loc, Some tac, punct) ->
      let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
      let status = eval_tactical status (tactic_of_ast' tac) in
-     (* CALL auto on every goal, easy way of testing it 
-     let auto = GrafiteAst.AutoBatch (loc, ([],["depth","1";"timeout","1"])) in
+     (* CALL auto on every goal, easy way of testing it *)
+     let auto = 
+       GrafiteAst.AutoBatch 
+         (loc, ([],["depth","1";"timeout","1";"type","1"])) in
      (try
        let auto = apply_tactic ~disambiguate_tactic ("",0,auto) in
        let _ = eval_tactical status (tactic_of_ast' auto) in ()
-     with _ -> ()); *)
+     with _ -> ());
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
   | GrafiteAst.Tactic (_, None, punct) ->
diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 415905258..8bd708eb7 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -181,14 +181,14 @@ distclean: clean
 
 TEST_DIRS = 				\
 	legacy                          \
-	library 			\
-	tests 				\
-	contribs/dama/dama		\
-	contribs/assembly		\
-	contribs/CoRN	 	        \
-	contribs/RELATIONAL	 	\
-	contribs/LOGIC	       	 	\
-	contribs/PREDICATIVE-TOPOLOGY 	\
+	library 			
+	# tests 				\
+	# contribs/dama/dama		\
+	# contribs/assembly		\
+	# contribs/CoRN	 	        \
+	# contribs/RELATIONAL	 	\
+	# contribs/LOGIC	       	 	\
+	# contribs/PREDICATIVE-TOPOLOGY 	\
 	$(NULL)
 
 #	library_auto