| TacticAst.Cut (_, term) -> Tactics.cut term
| TacticAst.Elim (_, term, _) ->
(* TODO Zack implement "using" argument *)
- Tactics.elim_intros_simpl term
+ (* old: Tactics.elim_intros_simpl term *)
+ Tactics.elim_intros term
| TacticAst.ElimType (_, term) -> Tactics.elim_type term
| TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
| TacticAst.Auto (_,num) ->