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 fd1eb34849b8a066796d3e81396d1fe756caf3e5..d85110774a5491ce07f34e8aa3291c0c5f8316fa 100644 (file)
--- 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 41590525815a2fbb3f4293e9831a41d6a7c3acaa..8bd708eb79ecee997915b0d7b310b625e5e1a1fd 100644 (file)
--- 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