-let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
- ?depth ?using what =
- let elim what = P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what in
- let elim_type_tac status =
- let tac = T.thens ~start: (P.cut_tac what)
- ~continuations:[elim (C.Rel 1); T.id_tac]
- in
- E.apply_tactic tac status
- in
- E.mk_tactic elim_type_tac
+let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
+ ?using what
+=
+ let elim what =
+ P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what
+ in
+ let elim_type_tac status =
+ let tac =
+ T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
+ in
+ E.apply_tactic tac status
+ in
+ E.mk_tactic elim_type_tac