Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / tactics / ring.ml

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index cf6950c4be9776a7d4de1ad309c1a29d4da8b6e2..4691239f411eb78362ce68dc29e839450675c6e2 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -495,7 +495,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 +538,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