int_of_string
(String.sub uri index_con (String.length uri - index_con)))
-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
- const ~subst uri
- else if sub = ".var" then
- var ~subst uri
- else
- (try
- (* Inductive Type *)
- let (uri, typeno) = indtyuri_of_uri s in
- mutind ~subst uri typeno
- with
- | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
- (* Constructor of an Inductive Type *)
- let (uri, typeno, consno) = indconuri_of_uri s in
- mutconstruct ~subst uri typeno consno)
- with
- | Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s)
-
(** {2 Helm's objects shorthands} *)
module Logic =
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