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
let attrs = [`Class (`InversionPrinciple); `Generated] in
let _subst = [] in
let proof=
- (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in
+ (Some inversor_uri,metasenv',_subst,
+ lazy (Cic.Meta(goal,[])),ref_theorem, attrs) in
let _,applies =
List.fold_right
(fun _ (i,applies) ->
Some
(inversor_uri,
Cic.Constant
- (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
+ (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[]))
with
Inversion.EqualityNotDefinedYet -> None
| CicRefine.RefineFailure ls ->