X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion_principle.ml;h=f2dd37f9eba744ffce46563f607abc1e8c0c8ba2;hb=10d3194c1b42dfa72e51000ff2cc217f937b43ac;hp=45ece4823a95caf0d54d9cf578841830f1962c40;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index 45ece4823..f2dd37f9e 100644
--- a/helm/software/components/tactics/inversion_principle.ml
+++ b/helm/software/components/tactics/inversion_principle.ml
@@ -195,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,_) ->