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
+ Inversion.EqualityNotDefinedYet -> None
+ | CicRefine.RefineFailure ls ->
+ HLog.warn
+ ("CicRefine.RefineFailure during generation of inversion principle: " ^
+ Lazy.force ls) ;
+ None
+ | CicRefine.Uncertain ls ->
+ HLog.warn
+ ("CicRefine.Uncertain during generation of inversion principle: " ^
+ Lazy.force ls) ;
+ None
+ | CicRefine.AssertFailure ls ->
+ HLog.warn
+ ("CicRefine.AssertFailure during generation of inversion principle: " ^
+ Lazy.force ls) ;
+ None
in
match obj with
| Cic.InductiveDefinition (tys,_,nleft,_) ->