int_of_string
(String.sub uri index_con (String.length uri - index_con)))
+(* (* NO LONGER USED, see CicUtil.term_of_uri *)
let term_of_uri ?(subst = []) uri =
let s = UriManager.string_of_uri uri in
try
(* Constant *)
- (* TODO explicit substitutions? *)
let len = String.length s in
let sub = String.sub s (len -4) 4 in
if sub = ".con" then
mutconstruct ~subst uri typeno consno)
with
| Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s)
+*)
(** {2 Helm's objects shorthands} *)
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
let rplus = const rplus_URI
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
module BinInt =
struct
+ let zmult_URI = uri "cic:/Coq/ZArith/BinInt/Zmult.con"
+ let zmult = const zmult_URI
let zplus_SURI = "cic:/Coq/ZArith/BinInt/Zplus.con"
let zplus_URI = uri zplus_SURI
let zplus = const zplus_URI
let zopp_SURI = "cic:/Coq/ZArith/BinInt/Zopp.con"
let zopp_URI = uri zopp_SURI
let zopp = const zopp_URI
+ let zpower_URI = uri "cic:/Coq/ZArith/Zpower/Zpower.con"
end
(** {2 Helpers for creating common terms}