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

3 files changed, 13 insertions, 10 deletions

diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index a35b6ffa42..d1910c1452 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -108,7 +108,8 @@ let dir_ml_load s =
 	 * if this code section starts to use a module not used elsewhere
 	 * in this file, the Makefile dependency logic needs to be updated.
 	 *)
-        let _,gname = where_in_path true !coq_mlpath_copy s in
+        let warn = Flags.is_verbose() in
+        let _,gname = where_in_path ~warn !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
 	with | Dynlink.Error a ->
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c7224ddaa8..aa519cd8ce 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -57,7 +57,9 @@ let real_error = function
    the file we parse seems a bit risky to me.  B.B.  *)
 
 let open_file_twice_if verbosely fname =
-  let _,longfname = find_file_in_path (Library.get_load_paths ()) fname in
+  let paths = Library.get_load_paths () in
+  let _,longfname =
+    find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
   let in_chan = open_in longfname in
   let verb_ch = if verbosely then Some (open_in longfname) else None in
   let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
@@ -131,7 +133,8 @@ let rec vernac_com interpfun (loc,com) =
         let cds = Dumpglob.coqdoc_freeze() in
           if !Flags.beautify_file then 
 	    begin
-              let _,f = find_file_in_path (Library.get_load_paths ())
+              let _,f = find_file_in_path ~warn:(Flags.is_verbose())
+		(Library.get_load_paths ())
 		(make_suffix fname ".v") in
 		chan_beautify := open_out (f^beautify_suffix);
 		Pp.comments := []
@@ -227,7 +230,7 @@ let load_vernac verb file =
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
-  let ldir,long_f_dot_v = Library.start_library f in
+  let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
     if Dumpglob.multi_dump () then 
       Dumpglob.open_glob_file (f ^ ".glob");
     Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ab3df8c0c3..39a545215b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -235,7 +235,7 @@ let dump_universes s =
 
 let locate_file f =
   try
-    let _,file = System.where_in_path false (Library.get_load_paths ()) f in
+    let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
     msgnl (str file)
   with Not_found -> 
     msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
@@ -592,11 +592,10 @@ let vernac_end_segment lid =
 
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
-  let modrefl = List.map Library.try_locate_qualified_library qidl in
-(*   let modrefl = List.map (fun qid -> let (dp, _) = (Library.try_locate_qualified_library qid) in dp) qidl in *)
-    if Dumpglob.dump () then
-      List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
-    Library.require_library_from_dirpath modrefl import
+  let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in
+  if Dumpglob.dump () then
+    List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
+  Library.require_library_from_dirpath modrefl import
 
 let vernac_canonical r =
   Recordops.declare_canonical_structure (global_with_alias r)