+let beta_after_elim_tac upto predicate =
+ let beta_after_elim_tac status =
+ let proof, goal = status in
+ let _, metasenv, _, _, _ = proof in
+ let _, _, ty = CicUtil.lookup_meta goal metasenv in
+ let mk_pattern ~equality ~upto ~predicate ty =
+ (* code adapted from ProceduralConversion.generalize *)
+ let meta = C.Implicit None in
+ let hole = C.Implicit (Some `Hole) in
+ let anon = C.Anonymous in
+ let is_meta =
+ let map b = function
+ | C.Implicit None when b -> b
+ | _ -> false
+ in
+ List.fold_left map true
+ in
+ let rec gen_fix len k (name, i, ty, bo) =
+ name, i, gen_term k ty, gen_term (k + len) bo
+ and gen_cofix len k (name, ty, bo) =
+ name, gen_term k ty, gen_term (k + len) bo
+ and gen_term k = function
+ | C.Sort _
+ | C.Implicit _
+ | C.Const (_, _)
+ | C.Var (_, _)
+ | C.MutInd (_, _, _)
+ | C.MutConstruct (_, _, _, _)
+ | C.Meta (_, _)
+ | C.Rel _ -> meta
+ | C.Appl (hd :: tl) when equality hd (S.lift k predicate) ->
+ assert (List.length tl = upto);
+ hole
+ | C.Appl ts ->
+ let ts = List.map (gen_term k) ts in
+ if is_meta ts then meta else C.Appl ts
+ | C.Cast (te, ty) ->
+ let te, ty = gen_term k te, gen_term k ty in
+ if is_meta [te; ty] then meta else C.Cast (te, ty)
+ | C.MutCase (sp, i, outty, t, pl) ->
+ let outty, t, pl = gen_term k outty, gen_term k t, List.map (gen_term k) pl in
+ if is_meta (outty :: t :: pl) then meta else hole (* C.MutCase (sp, i, outty, t, pl) *)
+ | C.Prod (_, s, t) ->
+ let s, t = gen_term k s, gen_term (succ k) t in
+ if is_meta [s; t] then meta else C.Prod (anon, s, t)
+ | C.Lambda (_, s, t) ->
+ let s, t = gen_term k s, gen_term (succ k) t in
+ if is_meta [s; t] then meta else C.Lambda (anon, s, t)
+ | C.LetIn (_, s, t) ->
+ let s, t = gen_term k s, gen_term (succ k) t in
+ if is_meta [s; t] then meta else C.LetIn (anon, s, t)
+ | C.Fix (i, fl) -> C.Fix (i, List.map (gen_fix (List.length fl) k) fl)
+ | C.CoFix (i, fl) -> C.CoFix (i, List.map (gen_cofix (List.length fl) k) fl)
+ in
+ None, [], Some (gen_term 0 ty)
+ in
+ let equality = CicUtil.alpha_equivalence in
+ let pattern = mk_pattern ~equality ~upto ~predicate ty in
+ let tactic = RT.head_beta_reduce_tac ~delta:false ~upto ~pattern in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic beta_after_elim_tac
+