X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Furimanager%2FuriManager.mli;h=703b0b4f1629e12639d64767a2c825b274fb49c8;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=2cdd27e3d386bd08ccd68b8bbc73a5d36b391ce5;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli
index 2cdd27e3d..703b0b4f1 100644
--- a/helm/ocaml/urimanager/uriManager.mli
+++ b/helm/ocaml/urimanager/uriManager.mli
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+exception IllFormedUri of string;;
+
 type uri
 
 val eq : uri -> uri -> bool
@@ -34,11 +36,6 @@ 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 *)
 
-(* relative_depth curi uri cookingsno                                        *)
-(* is the number of times to cook uri to use it when the current uri is curi *)
-(* cooked cookingsno times                                                   *)
-val relative_depth : uri -> uri -> int -> int
-
 (* given an uri, returns the uri of the corresponding cic file, *)
 (* i.e. removes the [.types][.ann] suffix                       *)
 val cicuri_of_uri : uri -> uri
@@ -49,3 +46,22 @@ val annuri_of_uri : uri -> uri
 
 (* given an uri, tells if it refers to an annotation *)
 val uri_is_annuri : 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 *)
+val bodyuri_of_uri : uri -> uri option
+
+(* 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 *)
+type uriref = uri * (int list)
+val string_of_uriref : uriref -> string
+