From 1db1b755ae0878041b3051886823275c19b01419 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 24 Feb 2004 15:45:31 +0000 Subject: [PATCH] New v8.0 URIs. --- helm/ocaml/tactics/ring.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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" -- 2.39.2