From a9051805b6d1be027d6695e300feb1b9efad9267 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 10 Sep 2008 13:02:09 +0000 Subject: [PATCH] AGAIN A TEST --- helm/software/components/grafite_engine/grafiteEngine.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index d85110774..aebae0387 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -800,11 +800,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status (* CALL auto on every goal, easy way of testing it *) let auto = GrafiteAst.AutoBatch - (loc, ([],["depth","1";"timeout","1";"type","1"])) in + (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 () - with _ -> ()); + 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