Porting URIs to V8.0.

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

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index bd9c1513661ba61d6abc8561cbb1ced948e7594e..fb5caa302cc85f59fb4292f2f36b94f7987f313f 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -190,7 +190,7 @@ exception GoalUnringable
   *)
 let ringable =
   let is_equality = function
-    | Cic.MutInd (uri, 0, []) when (eq uri Logic_Type.eqt_URI) -> true
+    | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true
     | _ -> false
   in
   let is_real = function
@@ -447,7 +447,7 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) =
   *)
 let ring_tac ~status:((proof, goal) as status) =
   warn "in Ring tactic";
-  let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in
+  let eqt = mkMutInd (Logic.eq_URI, 0) [] in
   let r = Reals.r in
   let metasenv = metasenv_of_status ~status in
   let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
@@ -473,7 +473,7 @@ let ring_tac ~status:((proof, goal) as status) =
             "exact sym_eqt su t1 ...", exact_tac
             ~term:(
               Cic.Appl
-               [mkConst Logic_Type.sym_eqt_URI
+               [mkConst Logic.sym_eq_URI
                  [equality_is_a_congruence_A, Reals.r;
                   equality_is_a_congruence_x, t1'' ;
                   equality_is_a_congruence_y, t1
@@ -511,7 +511,7 @@ let ring_tac ~status:((proof, goal) as status) =
                       exact_tac
                        ~term:(
                          Cic.Appl
-                          [mkConst Logic_Type.sym_eqt_URI
+                          [mkConst Logic.sym_eq_URI
                             [equality_is_a_congruence_A, Reals.r;
                              equality_is_a_congruence_x, t2'' ;
                              equality_is_a_congruence_y, t2