reverted previous fix

[helm.git] / components / tactics / inversion_principle.ml

diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml
index 1d56cab728770bd9eac6707080dde1b863599d30..f2dd37f9eba744ffce46563f607abc1e8c0c8ba2 100644 (file)
--- a/components/tactics/inversion_principle.ml
+++ b/components/tactics/inversion_principle.ml
@@ -8,7 +8,7 @@
  * modify it under the terms of the GNU General Public License
  * as published by the Free Software Foundation; either version 2
  * of the License, or (at your option) any later version.
-*
+ *
  * HELM is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
@@ -153,8 +153,10 @@ let build_inversion uri obj =
               UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
             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) in 
+              (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in 
             let _,applies =
               List.fold_right
                 (fun _ (i,applies) ->
@@ -184,8 +186,8 @@ let build_inversion uri obj =
                    ))
                 (proof,goal) 
             in
-            let metasenv,bo,ty =
-              match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty
+            let metasenv,bo,ty, attrs =
+              match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs
             in
               assert (metasenv = []);
               Some
@@ -193,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,_) ->