X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion_principle.ml;h=f2dd37f9eba744ffce46563f607abc1e8c0c8ba2;hb=ba5c1c83e77e701ef11625687ec27931bc4bb944;hp=b0f4d236ff5aa23e3fefad53b73e831c578e3274;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index b0f4d236f..f2dd37f9e 100644
--- a/helm/software/components/tactics/inversion_principle.ml
+++ b/helm/software/components/tactics/inversion_principle.ml
@@ -154,8 +154,9 @@ let build_inversion uri obj =
 	     let goal = CicMkImplicit.new_meta metasenv [] in
 	     let metasenv' = (goal,[],ref_theorem)::metasenv in
 	     let attrs = [`Class (`InversionPrinciple); `Generated] in
+       let _subst = [] in
 	     let proof= 
-	       (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem, attrs) in 
+	       (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in 
 	     let _,applies =
 	       List.fold_right
 		 (fun _ (i,applies) ->
@@ -186,7 +187,7 @@ let build_inversion uri obj =
 		 (proof,goal) 
 	     in
 	     let metasenv,bo,ty, attrs =
-	       match proof1 with (_,metasenv,bo,ty, attrs) -> metasenv,bo,ty, attrs
+	       match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs
 	     in
 	       assert (metasenv = []);
 	       Some
@@ -194,7 +195,22 @@ let build_inversion uri obj =
 		  Cic.Constant 
 		    (UriManager.name_of_uri inversor_uri,Some 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,_) ->