let lift_rewrite_tac ~context ~direction ~pattern equality =
let lift_rewrite_tac status =
let (proof, goal) = status in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
let n = List.length new_context - List.length context in
let equality = S.lift n equality in
let lift_destruct_tac ~context ~what =
let lift_destruct_tac status =
let (proof, goal) = status in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
let n = List.length new_context - List.length context in
let what = S.lift n what in
in
let subst_tac status =
let (proof, goal) = status in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let what = match PEH.get_rel context hyp with
| Some t -> t
| _ -> None
in
let (proof, goal) = status in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactics = HEL.list_rev_map_filter map context in
let result = PET.apply_tactic (T.seq ~tactics) status in