| C.ALambda (_, _, _, t) when n > 0 ->
aux 0 (pred n) (lift 1 (-1) t)
| t when n > 0 ->
| C.ALambda (_, _, _, t) when n > 0 ->
aux 0 (pred n) (lift 1 (-1) t)
| t when n > 0 ->
- let metasenv, ugraph = [], Un.oblivion_ugraph in
- let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
+ 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
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