]> matita.cs.unibo.it Git - helm.git/commitdiff
In some cases (e.g. JM equality) the inversion principle is not generated
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 18 May 2007 13:34:45 +0000 (13:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 18 May 2007 13:34:45 +0000 (13:34 +0000)
because CicRefine cannot infer a dependetly enough type. Now a warning is
raised and compilation is not stopped.

helm/software/components/tactics/inversion_principle.ml

index 45ece4823a95caf0d54d9cf578841830f1962c40..f2dd37f9eba744ffce46563f607abc1e8c0c8ba2 100644 (file)
@@ -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,_) ->