]> matita.cs.unibo.it Git - helm.git/blobdiff - components/extlib/hExtlib.mli
some work on making the compiler command line cleaner,
[helm.git] / components / extlib / hExtlib.mli
index 0d8d0aeff6951973cc0f606e6ff9201d31b61bff..73450ae11c62f7d860dcc9dface21a796767e132 100644 (file)
@@ -120,6 +120,12 @@ val raise_localized_exception: offset:int -> Stdpp.location -> exn -> 'a
 (* size in KB (SLOW) *)
 val estimate_size: 'a -> int
 
-(* is_prefix_of [prefix] [string] *)
+(* is_prefix_of [prefix] [string], in terms of dirs:
+ * foo/bar/ is prefix of foo/bar/baz 
+ * foo/bar  is prefix of foo/bar/baz 
+ * foo/b    isn't of     foo/bar/baz
+ * foo/bar  is prefix of foo/bar 
+ *)
 val is_prefix_of: string -> string -> bool
+val chop_prefix: string -> string -> string
 val touch: string -> unit