X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FhelmLibraryObjects.ml;h=ce81281a74a1ee48978d249c262c0606e25616a8;hb=ae1f66ceadc14c7d0824bb375c5af175b15f083c;hp=b2023b4487e95adedc3a53b287dc4904d9c2ed8b;hpb=0d6f26fe444a0a958eda5ac3a1efebca54de40ff;p=helm.git diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index b2023b448..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 @@ -147,9 +147,8 @@ module Peano = let ge_URI = uri ge_SURI let lt_SURI = "cic:/Coq/Init/Peano/lt.con" let lt_URI = uri lt_SURI - let gt_SURI = "cic:/Coq/Init/Peano/lt.con" + let gt_SURI = "cic:/Coq/Init/Peano/gt.con" let gt_URI = uri gt_SURI - let lt_URI = uri "cic:/Coq/Init/Peano/lt.con" let plus = const plus_URI let mult = const mult_URI