From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 24 Feb 2004 15:45:31 +0000 (+0000)
Subject: New v8.0 URIs.
X-Git-Tag: v0_0_4~84
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=1db1b755ae0878041b3051886823275c19b01419;p=helm.git

New v8.0 URIs.
---

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"