+ gen_term
+
+let convert g ety k predicate =
+ let rec aux = function
+ | C.ALambda (_, _, b, ety), C.ALambda (id, n, u, pred) ->
+ C.ALambda (id, n, aux (b, u), aux (ety, pred))
+ | C.AProd (_, _, b, ety), C.AProd (id, n, u, pred) ->
+ C.AProd (id, n, aux (b, u), aux (ety, pred))
+ | C.ALetIn (_, _, a, b, ety), C.ALetIn (id, n, v, u, pred) ->
+ C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ety, pred))
+ | C.AAppl (_, bs), C.AAppl (id, us) when List.length bs = List.length us ->
+ let map b u = aux (b,u) in
+ C.AAppl (id, List.map2 map bs us)
+ | C.ACast (_, ety, b), C.ACast (id, pred, u) ->
+ C.ACast (id, aux (ety, pred), aux (b, u))
+ | ety, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) ->
+ aux (ety, subst 1 v pred)
+ | ety, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) ->
+ aux (ety, C.AAppl (id, subst 1 v pred :: vs))
+ | _, pred -> pred
+ in
+ g k (aux (ety, predicate))
+
+let mk_pattern psno ety predicate =
+ clear_absts (convert (generalize psno) ety) psno 0 predicate
+
+let get_clears c p xtypes =
+ let meta = C.Implicit None in
+ let rec aux c names p it et = function
+ | [] ->
+ List.rev c, List.rev names
+ | Some (C.Name name as n, C.Decl v) as hd :: tl ->
+ let hd, names, v =
+ if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then
+ Some (C.Anonymous, C.Decl v), name :: names, meta
+ else
+ hd, names, v
+ in
+ let p = C.Lambda (n, v, p) in
+ let it = C.Prod (n, v, it) in
+ let et = C.Prod (n, v, et) in
+ aux (hd :: c) names p it et tl
+ | Some (C.Name name as n, C.Def (v, x)) as hd :: tl ->
+ let hd, names, v =
+ if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then
+ Some (C.Anonymous, C.Def (v, x)), name :: names, meta
+ else
+ hd, names, v
+ in
+ let p = C.LetIn (n, v, x, p) in
+ let it = C.LetIn (n, v, x, it) in
+ let et = C.LetIn (n, v, x, et) in
+ aux (hd :: c) names p it et tl
+ | Some (C.Anonymous as n, C.Decl v) as hd :: tl ->
+ let p = C.Lambda (n, meta, p) in
+ let it = C.Lambda (n, meta, it) in
+ let et = C.Lambda (n, meta, et) in
+ aux (hd :: c) names p it et tl
+ | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
+ let p = C.LetIn (n, meta, meta, p) in
+ let it = C.LetIn (n, meta, meta, it) in
+ let et = C.LetIn (n, meta, meta, et) in
+ aux (hd :: c) names p it et tl
+ | None :: tl -> assert false
+ in
+ match xtypes with
+ | Some (it, et) -> aux [] [] p it et c
+ | None -> c, []
+
+let clear c hyp =
+ let rec aux c = function
+ | [] -> List.rev c
+ | Some (C.Name name, entry) :: tail when name = hyp ->
+ aux (Some (C.Anonymous, entry) :: c) tail
+ | entry :: tail -> aux (entry :: c) tail
+ in
+ aux [] c
+
+let elim_inferred_type context goal arg using cpattern =
+ let metasenv, ugraph = [], Un.default_ugraph in
+ let ety = H.get_type "elim_inferred_type" context using in
+ let _splits, args_no = PEH.split_with_whd (context, ety) in
+ let _metasenv, _subst, predicate, _arg, actual_args =
+ PT.mk_predicate_for_elim
+ ~context ~metasenv ~subst:[] ~ugraph ~goal ~arg ~using ~cpattern ~args_no
+ in
+ let ty = C.Appl (predicate :: actual_args) in
+ let upto = List.length actual_args in
+ Rd.head_beta_reduce ~delta:false ~upto ty