- let pattern = None, PEH.list_rev_map_filter (map hyp) context, Some hole in
- let start = rewrite_tac ~direction ~pattern what in
- let continuation = PESR.clear ~hyps:[hyp; var] in
- let tac = T.then_ ~start ~continuation in
- PET.apply_tactic tac status
+ let map self = function
+ | Some (C.Name s, _) when s <> self ->
+ Some (rewrite (None, [(s, hole)], None))
+ | _ -> None
+ in
+ let rew_hips = HEL.list_rev_map_filter (map hyp) context in
+ let rew_concl = rewrite (None, [], Some hole) in
+ let clear = PESR.clear ~hyps:[hyp; var] in
+ let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in
+ PET.apply_tactic (T.seq ~tactics) status
+ in
+ PET.mk_tactic subst_tac
+
+let subst_tac =
+ let subst hyp = try_tactic ~tactic:(subst_tac hyp) in
+ let map = function
+ | Some (C.Name s, _) -> Some (subst s)
+ | _ -> None
+ in
+ let subst_tac status =
+ let (proof, goal) = status in
+ let (_, metasenv, _, _) = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let tactics = HEL.list_rev_map_filter map context in
+ PET.apply_tactic (T.seq ~tactics) status