From 47988107f44566d53fd5a71fd64a015bbf24a380 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 May 2007 13:34:45 +0000 Subject: [PATCH] In some cases (e.g. JM equality) the inversion principle is not generated because CicRefine cannot infer a dependetly enough type. Now a warning is raised and compilation is not stopped. --- .../components/tactics/inversion_principle.ml | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) 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,_) -> -- 2.39.2