From c3b4dfecb4ead05a2e008dca9abc24a6c7803ddc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 26 Sep 2008 09:05:17 +0000 Subject: [PATCH] iremoved call to auto --- helm/software/components/grafite_engine/grafiteEngine.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 888ad55ff..887e767e6 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -797,16 +797,15 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | 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 (try let auto = apply_tactic ~disambiguate_tactic ("",0,auto) in let _ = eval_tactical status (tactic_of_ast' auto) in - print_endline "GOOD"; () - with ProofEngineTypes.Fail _ -> print_endline "BAD" | _ -> ()); - *) + 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.5