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
[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)