| None,_
| _,None -> assert false
| Some proof', Some goal' ->
- let (newproof, newgoals) = tactic ~status:(proof', goal') in
+ let (newproof, newgoals) = tactic (proof', goal') in
set_proof (Some newproof);
goal :=
(match newgoals, newproof with
let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
+let auto mqi_handle () = apply_tactic (VariousTactics.auto_tac mqi_handle)
let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)