]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/urimanager/uriManager.mli
relativeDepth function removed (useful only for cooking)
[helm.git] / helm / ocaml / urimanager / uriManager.mli
index 8afb4e345ac28ee3d29ed6ecad88ff1af97eaf33..0f4f15ea2822ce998847a7312759a7352dfb397f 100644 (file)
@@ -36,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