New v8.0 URIs.

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index fb5caa302cc85f59fb4292f2f36b94f7987f313f..f9755474c0a59cdd418665328ca663f7d542fbb1 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -49,11 +49,11 @@ let warn s =
 *)
 
 let equality_is_a_congruence_A =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var"
 let equality_is_a_congruence_x =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var"
 let equality_is_a_congruence_y =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var"
 
 let apolynomial_uri =
   uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"