]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/urimanager/uriManager.mli
debian: rebuilt against ocaml 3.08.2
[helm.git] / helm / ocaml / urimanager / uriManager.mli
index 0f4f15ea2822ce998847a7312759a7352dfb397f..12775af8d48fd9a3168fbc149bfc7ebbf7ec4766 100644 (file)
@@ -40,6 +40,8 @@ val depth_of_uri  : uri -> int     (* length of the path *)
 (* i.e. removes the [.types][.ann] suffix                       *)
 val cicuri_of_uri : uri -> uri
 
+val strip_xpointer: uri -> uri      (* remove trailing #xpointer..., if any *)
+
 (* given an uri, returns the uri of the corresponding annotation file, *)
 (* i.e. adds the .ann suffix if not already present                    *)
 val annuri_of_uri : uri -> uri
@@ -53,3 +55,15 @@ 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
+