-let elim_intros_tac ~term =
- Tacticals.then_ ~start:(elim_tac ~term)
- ~continuation:(intros_tac ())
+let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ ?depth ?using what =
+ Tacticals.then_ ~start:(elim_tac ~term:what)
+ ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())