From b77a92a67de2e403d03e452ed6f63911002ee717 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Jun 2004 08:43:42 +0000 Subject: [PATCH] Fourier URIs changed in V8. --- helm/ocaml/cic/helmLibraryObjects.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 88ff7574d..ce81281a7 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -118,8 +118,8 @@ module Reals = let rlt_URI = uri rlt_SURI let rgt_SURI = "cic:/Coq/Reals/Rdefinitions/Rgt.con" let rgt_URI = uri rgt_SURI - let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con" - let rinv_r1_URI = uri "cic:/Coq/Reals/Rbase/Rinv_R1.con" + let rtheory_URI = uri "cic:/Coq/Reals/RIneq/RTheory.con" + let rinv_r1_URI = uri "cic:/Coq/Reals/RIneq/Rinv_1.con" let pow_URI = uri "cic:/Coq/Reals/Rfunctions/pow.con" let r = const r_URI -- 2.39.2