+(* FG: This should be replaced by T.try_tactic *)
+let try_tactic ~tactic =
+ let try_tactic status =
+ try PET.apply_tactic tactic status with
+ | PET.Fail _ -> PET.apply_tactic T.id_tac status
+ in
+ PET.mk_tactic try_tactic
+
+let rec lift_rewrite_tac ~context ~direction ~pattern equality =
+ let lift_rewrite_tac status =
+ let (proof, goal) = status in
+ let (_, metasenv, _, _) = proof in
+ let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
+ let n = List.length new_context - List.length context in
+ let equality = if n > 0 then S.lift n equality else equality in
+ PET.apply_tactic (rewrite_tac ~direction ~pattern equality) status
+ in
+ PET.mk_tactic lift_rewrite_tac
+
+