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