Backporting from v8.2 to trunk:

- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 4 deletions

diff --git a/lib/system.mli b/lib/system.mli
index 48e02cb5d..7556ed9e4 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -22,7 +22,7 @@ val exclude_search_in_dirname : string -> unit
 
 val all_subdirs : unix_path:string -> (physical_path * string list) list
 val is_in_path : load_path -> string -> bool
-val where_in_path : bool -> load_path -> string -> physical_path * string
+val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string
 
 val physical_path_of_string : string -> physical_path
 val string_of_physical_path : physical_path -> string
@@ -36,7 +36,8 @@ val home : string
 
 val exists_dir : string -> bool
 
-val find_file_in_path : load_path -> string -> physical_path * string
+val find_file_in_path :
+  ?warn:bool -> load_path -> string -> physical_path * string
 
 (*s Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
@@ -50,8 +51,8 @@ exception Bad_magic_number of string
 val raw_extern_intern : int -> string -> 
   (string -> string * out_channel) * (string -> in_channel)
 
-val extern_intern : 
-  int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a)
+val extern_intern : ?warn:bool -> int -> string -> 
+  (string -> 'a -> unit) * (load_path -> string -> 'a)
 
 (*s Sending/receiving once with external executable *)