type uri
val eq : uri -> uri -> bool
+val compare : uri -> uri -> int
val uri_of_string : string -> uri
val string_of_uri : uri -> string (* complete uri *)
val name_of_uri : uri -> string (* name only (without extension)*)
-val buri_of_uri : uri -> string (* base uri only *)
-val depth_of_uri : uri -> int (* length of the path *)
+val buri_of_uri : uri -> string (* base uri only, without trailing '/' *)
(* given an uri, returns the uri of the corresponding cic file, *)
(* i.e. removes the [.types][.ann] suffix *)
(* i.e. adds the .ann suffix if not already present *)
val annuri_of_uri : uri -> uri
-(* given an uri, tells if it refers to an annotation *)
val uri_is_annuri : uri -> bool
+val uri_is_var : uri -> bool
+val uri_is_con : uri -> bool
+val uri_is_ind : uri -> bool
(* given an uri of a constant, it gives back the uri of its body *)
(* it gives back None if the uri refers to a Variable or MutualInductiveType *)
(* given an uri, it gives back the uri of its inner types *)
val innertypesuri_of_uri : uri -> uri
-(*
-val mutind_uri: uri -> int -> uri
-val mutconstruct_uri: uri -> int -> int -> uri
-val mutind: uri -> uri * int
-val mutconstruct: uri -> uri * int * int
-*)
+(* builder for MutInd and MutConstruct URIs
+ * [uri] -> [typeno] -> [consno option]
+ *)
+val uri_of_uriref : uri -> int -> int option -> uri
- (* builder for MutInd and MutConstruct URIs *)
-type uriref = uri * (int list)
-val string_of_uriref : uriref -> string
+module UriSet: Set.S with type elt = uri