X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fring.ml;h=82ef5f4f2b239a3cfed99092230632e180e51709;hb=af805d8cb199ea2c532983e29b064cf9861454f4;hp=7695a4ff0c82d885b66c9a76f1a3478cd915823b;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/ring.ml b/helm/software/components/tactics/ring.ml
index 7695a4ff0..82ef5f4f2 100644
--- a/helm/software/components/tactics/ring.ml
+++ b/helm/software/components/tactics/ring.ml
@@ -503,7 +503,7 @@ let ring_tac status =
               let status' = (* status after 1st elim_type use *)
                 let context = context_of_status status in
 		let b,_ = (*TASSI : FIXME*)
-		  are_convertible context t1'' t1 CicUniv.empty_ugraph in 
+		  are_convertible context t1'' t1 CicUniv.oblivion_ugraph in 
                 if not b then begin
                   warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
                   let newstatus =
@@ -544,7 +544,8 @@ let ring_tac status =
                       let status' =
                         let context = context_of_status status in
 			let b,_ = (* TASSI:FIXME *)
-			  are_convertible context t2'' t2 CicUniv.empty_ugraph 
+			  are_convertible context t2'' t2
+                          CicUniv.oblivion_ugraph 
 			in
 			  if not b then begin 
                           warn (lazy "t2'' and t2 are NOT CONVERTIBLE");