else
hd, names, v
in
- let p = C.LetIn (n, v, assert false, p) in
- let it = C.LetIn (n, v, assert false, it) in
- let et = C.LetIn (n, v, assert false, et) 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 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, assert false, p) in
- let it = C.LetIn (n, meta, assert false, it) in
- let et = C.LetIn (n, meta, assert false, et) in
+ 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
aux [] c
let elim_inferred_type context goal arg using cpattern =
- let metasenv, ugraph = [], Un.empty_ugraph in
+ let metasenv, ugraph = [], Un.oblivion_ugraph in
let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
let _splits, args_no = PEH.split_with_whd (context, ety) in
let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim