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 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