]> matita.cs.unibo.it Git - helm.git/commitdiff
More v8.0 URIs.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 24 Feb 2004 15:21:40 +0000 (15:21 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 24 Feb 2004 15:21:40 +0000 (15:21 +0000)
helm/ocaml/cic/helmLibraryObjects.ml

index 3ff0163d2c6880b4520af7c8698e5c66ce092a4b..913fc9ef30f68ae0516b7dc56918a380b1ae63fb 100644 (file)
@@ -96,15 +96,20 @@ module Reals =
     let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con"
     let rplus_SURI = "cic:/Coq/Reals/Rdefinitions/Rplus.con"
     let rplus_URI = uri rplus_SURI
-    let rminus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rminus.con"
-    let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con"
-    let rdiv_URI = uri "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
+    let rminus_SURI = "cic:/Coq/Reals/Rdefinitions/Rminus.con"
+    let rminus_URI = uri rminus_SURI
+    let rmult_SURI = "cic:/Coq/Reals/Rdefinitions/Rmult.con"
+    let rmult_URI = uri rmult_SURI
+    let rdiv_SURI = "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
+    let rdiv_URI = uri rdiv_SURI
     let ropp_SURI = "cic:/Coq/Reals/Rdefinitions/Ropp.con"
     let ropp_URI = uri ropp_SURI
     let rinv_SURI = "cic:/Coq/Reals/Rdefinitions/Rinv.con"
     let rinv_URI = uri rinv_SURI
-    let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con"
-    let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con"
+    let r0_SURI = "cic:/Coq/Reals/Rdefinitions/R0.con"
+    let r0_URI = uri r0_SURI
+    let r1_SURI = "cic:/Coq/Reals/Rdefinitions/R1.con"
+    let r1_URI = uri r1_SURI
     let rle_SURI = "cic:/Coq/Reals/Rdefinitions/Rle.con"
     let rle_URI = uri rle_SURI
     let rge_SURI = "cic:/Coq/Reals/Rdefinitions/Rge.con"
@@ -129,8 +134,10 @@ module Peano =
   struct
     let plus_SURI = "cic:/Coq/Init/Peano/plus.con"
     let plus_URI = uri plus_SURI
-    let minus_URI = uri "cic:/Coq/Init/Peano/minus.con"
-    let mult_URI = uri "cic:/Coq/Init/Peano/mult.con"
+    let minus_SURI = "cic:/Coq/Init/Peano/minus.con"
+    let minus_URI = uri minus_SURI
+    let mult_SURI = "cic:/Coq/Init/Peano/mult.con"
+    let mult_URI = uri mult_SURI
     let pred_URI = uri "cic:/Coq/Init/Peano/pred.con"
     let le_SURI = "cic:/Coq/Init/Peano/le.ind"
     let le_URI = uri le_SURI