-
-let elim_type_tac ~term ~status =
- let module C = Cic in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- T.thens
- ~start: (P.cut_tac term)
- ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
- ~status
+let elim_type_tac ~term =
+ let elim_type_tac ~term status =
+ let module C = Cic in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ ProofEngineTypes.apply_tactic
+ (T.thens
+ ~start: (P.cut_tac term)
+ ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ])
+ status
+ in
+ ProofEngineTypes.mk_tactic (elim_type_tac ~term)