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
let rec subst_tac ~try_tactic ~hyp =
let hole = C.Implicit (Some `Hole) in
let meta = C.Implicit None in
+ let rec ind = function
+ | C.MutInd _ -> true
+ | C.Appl (t :: tl) -> ind t
+ | _ -> false
+ in
let rec constr = function
| C.MutConstruct _ -> true
| C.Appl (t :: tl) -> constr t
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
[lift_destruct_tac ~context ~what; PESR.clear ~hyps:[hyp]]
in
let whd_g () =
- let whd_pattern = C.Appl [meta; meta; hole; hole] in
+ let whd_pattern = C.Appl [meta; hole; hole; hole] in
let pattern = None, [hyp, whd_pattern], None in
[RT.whd_tac ~pattern; subst_tac ~try_tactic ~hyp]
in
when LO.is_eq_URI uri -> subst_g `LeftToRight i t
| (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i])
when LO.is_eq_URI uri -> subst_g `RightToLeft i t
- | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2])
- when LO.is_eq_URI uri && constr t1 && constr t2 -> destruct_g ()
+ | (C.Appl [(C.MutInd (uri, 0, [])); t; t1; t2])
+ when LO.is_eq_URI uri && ind t && constr t1 && constr t2 -> destruct_g ()
| (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2])
when LO.is_eq_URI uri -> whd_g ()
| _ -> raise (PET.Fail msg1)
| _ -> 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