X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion_principle.ml;h=0f50116cb5ed7be0ce46d09178e8317a8dc1f8fe;hb=0b76904a3f10bfd6390d26172fd6979626bd72f4;hp=1d56cab728770bd9eac6707080dde1b863599d30;hpb=2aad3e4b468d3e4199712437e7ef82afbbc9553d;p=helm.git

diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index 1d56cab72..0f50116cb 100644
--- a/helm/software/components/tactics/inversion_principle.ml
+++ b/helm/software/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
@@ -145,7 +145,7 @@ let build_inversion uri obj =
 	   debug_print 
 	     (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
 	   let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem  
-	     CicUniv.empty_ugraph in
+	     CicUniv.oblivion_ugraph in
 	     (*DEBUG*) debug_print 
 	     (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
 	     let buri = UriManager.buri_of_uri uri in
@@ -153,8 +153,11 @@ 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,
+                 lazy (Cic.Meta(goal,[])),ref_theorem, attrs) in 
 	     let _,applies =
 	       List.fold_right
 		 (fun _ (i,applies) ->
@@ -184,16 +187,31 @@ 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
 		 (inversor_uri,
 		  Cic.Constant 
-		    (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
+		    (UriManager.name_of_uri inversor_uri,Some (Lazy.force 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,_) ->