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