- let (proof',goals) =
- PET.apply_tactic
- (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty),goal)
- in
- let goals =
- goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
- ~newmetasenv:metasenv')
- in
- (proof',goals)
- 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)
+ try
+ let (proof',goals) =
+ PET.apply_tactic
+ (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal)
+ in
+ let goals =
+ goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+ ~newmetasenv:metasenv')
+ in
+ (proof',goals)
+ with (* FG: this should be PET.Fail _ *)
+ TC.TypeCheckerFailure m ->
+ let msg = lazy ("rewrite: "^ Lazy.force m) in
+ raise (PET.Fail msg)
+ 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)