X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion_principle.ml;h=2b6e14b37e28e5ccc3a515ce0f5a1d86c727b685;hb=e48ac5af4e17dbac21b7e2767d4bd17f47ab19ea;hp=f2dd37f9eba744ffce46563f607abc1e8c0c8ba2;hpb=47988107f44566d53fd5a71fd64a015bbf24a380;p=helm.git

diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index f2dd37f9e..2b6e14b37 100644
--- a/helm/software/components/tactics/inversion_principle.ml
+++ b/helm/software/components/tactics/inversion_principle.ml
@@ -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