From 7d5e6494f7598a5b1a0486526fcc804dae6e7d9b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 10 Sep 2008 13:10:27 +0000 Subject: [PATCH] reverted auto experiment --- helm/software/components/grafite_engine/grafiteEngine.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index aebae0387..10cf1b8cb 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -794,10 +794,10 @@ 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 *) + (* CALL auto on every goal, easy way of testing it let auto = GrafiteAst.AutoBatch (loc, ([],["depth","2";"timeout","1";"type","1"])) in @@ -806,6 +806,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let _ = eval_tactical status (tactic_of_ast' auto) in print_endline "GOOD"; () with ProofEngineTypes.Fail _ -> print_endline "BAD" | _ -> ()); + *) eval_tactical status (punctuation_tactical_of_ast (text,prefix_len,punct)),[] | GrafiteAst.Tactic (_, None, punct) -> -- 2.39.2