This commit was manufactured by cvs2svn to create branch 'helm'.

[helm.git] / helm / interface / uriManager.mli

diff --git a/helm/interface/uriManager.mli b/helm/interface/uriManager.mli
deleted file mode 100644 (file)
index 8cffc94..0000000
--- a/helm/interface/uriManager.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-type uri
-
-val eq : uri -> uri -> bool
-
-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 *)
-
-(* 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