X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion_principle.ml;h=0f50116cb5ed7be0ce46d09178e8317a8dc1f8fe;hb=45a9e84c12f57e5473eccc6f611cdbb343998d5d;hp=2b6e14b37e28e5ccc3a515ce0f5a1d86c727b685;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index 2b6e14b37..0f50116cb 100644
--- a/helm/software/components/tactics/inversion_principle.ml
+++ b/helm/software/components/tactics/inversion_principle.ml
@@ -156,7 +156,8 @@ let build_inversion uri obj =
 	     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) ->
@@ -193,7 +194,7 @@ let build_inversion uri obj =
 	       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 ->