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"
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