X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2Fring.ml;h=cebb4cf91b35416d73a637cbf73a7aabb5861136;hb=fc9cad6c109e279130501114000edcfb9621075b;hp=cf6950c4be9776a7d4de1ad309c1a29d4da8b6e2;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index cf6950c4b..cebb4cf91 100644
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -34,11 +34,12 @@ open HelmLibraryObjects
 
   (** perform debugging output? *)
 let debug = false
+let debug_print = fun _ -> ()
 
   (** debugging print *)
 let warn s =
   if debug then
-    prerr_endline ("RING WARNING: " ^ s)
+    debug_print ("RING WARNING: " ^ s)
 
 (** CIC URIS *)
 
@@ -495,7 +496,9 @@ let ring_tac status =
             "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
               let status' = (* status after 1st elim_type use *)
                 let context = context_of_status status in
-                if not (are_convertible context t1'' t1) then begin
+		let b,_ = (*TASSI : FIXME*)
+		  are_convertible context t1'' t1 CicUniv.empty_ugraph in 
+                if not b then begin
                   warn "t1'' and t1 are NOT CONVERTIBLE";
                   let newstatus =
 		    ProofEngineTypes.apply_tactic 
@@ -536,7 +539,10 @@ let ring_tac status =
 		     ProofEngineTypes.mk_tactic (fun status ->
                       let status' =
                         let context = context_of_status status in
-                        if not (are_convertible context t2'' t2) then begin
+			let b,_ = (* TASSI:FIXME *)
+			  are_convertible context t2'' t2 CicUniv.empty_ugraph 
+			in
+			  if not b then begin 
                           warn "t2'' and t2 are NOT CONVERTIBLE";
                           let newstatus =
 			    ProofEngineTypes.apply_tactic