- ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
-;;
-
-let rewrite_back_tac ?where ~term () =
- let rewrite_back_tac ?where ~term status =
- rewrite ?where ~term ~direction:`Left status
- in
- ProofEngineTypes.mk_tactic (rewrite_back_tac ?where ~term)
-
-let rewrite_back_simpl_tac ?where ~term () =
- let rewrite_back_simpl_tac ?where ~term status =
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(rewrite_back_tac ?where ~term ())
- ~continuation:
- (ReductionTactics.simpl_tac
- ~pattern:(ProofEngineTypes.conclusion_pattern None)))
- status
- in
- ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)