- Tacticals.thens ~start:(E.elim_type_tac ~term)
- ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] status
+ ProofEngineTypes.apply_tactic
+ (Tacticals.thens ~start:(E.elim_type_tac ~term)
+ ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
+ in
+ ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)