let refine_term metasenv context uri term ugraph ~localization_tbl =
(* if benchmark then incr actual_refinements; *)
- assert (uri=None);
+ assert (uri=None);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
try
let term', _, metasenv',ugraph1 =
CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
debug_print (lazy (sprintf "OK!!!"));
- Ok (term', metasenv',ugraph1)
+ Ok (term', metasenv',ugraph1)
with
exn ->
let rec process_exn loc =