let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
try
- let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in
+ let term', _, metasenv' = CicRefine.type_of_aux' metasenv context term in
Ok (term', metasenv')
with
| CicRefine.Uncertain _ ->