+let mk_pattern psno predicate =
+ let body = generalize psno predicate in
+ clear_absts 0 psno body
+
+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, predicate, _arg, actual_args = PT.mk_predicate_for_elim
+ ~context ~metasenv ~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
+
+let does_not_occur = function
+ | C.AImplicit (_, None) -> true
+ | _ -> false