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 ->