| tac -> tac
in
let needed_by_script ast =
- prerr_endline (TacticAstPp.pp_tactical ast);
match strip_locations ast with
| A.Tactic _
| A.Command
| _ -> false
in
let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in
+ debug_print (sprintf "evaluating '%s'" s);
if needed_by_script ast then
- script#advance ast
+ script#advance s
else
interpreter#evalAst ast
let hole = CicAst.UserInput in
let tac ast _ =
let ast = A.Tactic ast in
- ignore (interpreter#evalAst ast);
- ignore (script#advance ast)
+ ignore (script#advance (TacticAstPp.pp_tactical ast))
in
let tac_w_term ast _ =
(* gui#console#clear (); *)