X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;fp=helm%2Focaml%2Ftactics%2Fring.ml;h=f9755474c0a59cdd418665328ca663f7d542fbb1;hb=1db1b755ae0878041b3051886823275c19b01419;hp=fb5caa302cc85f59fb4292f2f36b94f7987f313f;hpb=619e54333d7ba0aa934820bd03d7e0ee2e19b3ac;p=helm.git

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index fb5caa302..f9755474c 100644
--- 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"