debug_print
(lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
(*DEBUG*) debug_print
(lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
let buri = UriManager.buri_of_uri uri in