- in
- ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
-
-
-let rewrite_simpl_tac ~direction ~pattern equality =
- let rewrite_simpl_tac ~direction ~pattern equality status =
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(rewrite_tac ~direction ~pattern equality)
+ in
+ PET.mk_tactic _rewrite_tac
+
+let rewrite_tac ~direction ~pattern equality names =
+ let _, hyps_pat, _ = pattern in
+ let froms = List.map fst hyps_pat in
+ let start = rewrite_tac ~direction ~pattern equality in
+ let continuation = PESR.rename ~froms ~tos:names in
+ if names = [] then start else T.then_ ~start ~continuation
+
+let rewrite_simpl_tac ~direction ~pattern equality names =
+ T.then_
+ ~start:(rewrite_tac ~direction ~pattern equality names)