Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

32 files changed, 291 insertions, 222 deletions

diff --git a/tools/compat5.ml b/tools/compat5.ml
index 041ced0044..33c1cd602b 100644
--- a/tools/compat5.ml
+++ b/tools/compat5.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5.mlp b/tools/compat5.mlp
index 91e3cdae5f..8473a1fb7f 100644
--- a/tools/compat5.mlp
+++ b/tools/compat5.mlp
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
index a2336e1015..37cb487c59 100644
--- a/tools/compat5b.ml
+++ b/tools/compat5b.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp
index d4dfcc07d0..46802a8259 100644
--- a/tools/compat5b.mlp
+++ b/tools/compat5b.mlp
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4b92d57082..7b76514e46 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -43,6 +43,16 @@ let section s =
   print_com (String.make (l+2) '#');
   print "\n"
 
+(* These are the Coq library directories that are used for
+ * plugin development
+ *)
+let lib_dirs =
+  ["kernel"; "lib"; "library"; "parsing";
+   "pretyping"; "interp"; "printing"; "intf";
+   "proofs"; "tactics"; "tools"; "toplevel";
+   "stm"; "grammar"; "config"; "ltac"; "engine"]
+
+
 let usage () =
   output_string stderr "Usage summary:
 
@@ -99,7 +109,13 @@ let string_prefix a b =
 let is_prefix dir1 dir2 =
   let l1 = String.length dir1 in
   let l2 = String.length dir2 in
-    dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/')
+  let sep = Filename.dir_sep in
+  if dir1 = dir2 then true
+  else if l1 + String.length sep <= l2 then
+    let dir1' = String.sub dir2 0 l1 in
+    let sep' = String.sub dir2 l1 (String.length sep) in
+    dir1' = dir1 && sep' = sep
+  else false
 
 let physical_dir_of_logical_dir ldir =
   let le = String.length ldir - 1 in
@@ -446,12 +462,8 @@ let variables is_install opt (args,defs) =
     end;
     (* Caml executables and relative variables *)
     if !some_ml4file || !some_mlfile || !some_mlifile then begin
-    print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\
-  -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)engine\" -I \"$(COQLIB)pretyping\" \\
-  -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\
-  -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\
-  -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\" \\
-  -I \"$(COQLIB)config\"";
+    print "COQSRCLIBS?=" ;
+    List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ;
     List.iter (fun c -> print " \\
   -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
@@ -508,7 +520,7 @@ let parameters () =
   print "define donewline\n\n\nendef\n";
   print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n";
   print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
-  print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
+  print "TIMED?=\nTIMECMD?=\nSTDTIME=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
   print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
   print "vo_to_obj = $(addsuffix .o,\\\n";
   print "  $(filter-out Warning: Error:,\\\n";
@@ -770,7 +782,7 @@ let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l
 	&& not_tops mllib && not_tops mlpack) then
     l
   else
-    ((".",here)::ml_inc,(".","Top",here)::i_inc,r_inc)
+    ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc)
 
 let warn_install_at_root_directory
     (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) =
@@ -794,6 +806,21 @@ let check_overlapping_include (_,inc_i,inc_r) =
 	    Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l;
   in aux (inc_i@inc_r)
 
+(* Generate a .merlin file that references the standard library and
+ * any -I included paths.
+ *)
+let merlin targets (ml_inc,_,_) =
+  print ".merlin:\n";
+  print "\t@echo 'FLG -rectypes' > .merlin\n" ;
+  List.iter (fun c ->
+      printf "\t@echo \"B $(COQLIB) %s\" >> .merlin\n" c)
+    lib_dirs ;
+  List.iter (fun (_,c) ->
+      printf "\t@echo \"B %s\" >> .merlin\n" c;
+      printf "\t@echo \"S %s\" >> .merlin\n" c)
+    ml_inc;
+  print "\n"
+
 let do_makefile args =
   let has_file var = function
     |[] -> var := false
@@ -836,6 +863,7 @@ let do_makefile args =
   section "Special targets.";
   standard opt;
   install targets inc is_install;
+  merlin targets inc;
   clean sds sps;
   make_makefile sds;
   implicit ();
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index dbdc2e9db1..e17011b39a 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5710b97f2a..f957200ab5 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -30,13 +30,8 @@ let verbose = ref false
 let rec make_compilation_args = function
   | [] -> []
   | file :: fl ->
-      let file_noext =
-        if Filename.check_suffix file ".v" then
-          Filename.chop_suffix file ".v"
-        else file
-      in
       (if !verbose then "-compile-verbose" else "-compile")
-      :: file_noext :: (make_compilation_args fl)
+      :: file :: (make_compilation_args fl)
 
 (* compilation of files [files] with command [command] and args [args] *)
 
@@ -75,17 +70,6 @@ let parse_args () =
     | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem
     | "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem
 
-(* Obsolete options *)
-
-    | "-libdir" :: _ :: rem ->
-        print_string "Warning: option -libdir deprecated and ignored\n";
-        flush stdout;
-        parse (cfiles,args) rem
-    | ("-db"|"-debugger") :: rem ->
-        print_string "Warning: option -db/-debugger deprecated and ignored\n";
-        flush stdout;
-        parse (cfiles,args) rem
-
 (* Informative options *)
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
@@ -129,21 +113,11 @@ let parse_args () =
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
 	    | []        -> usage ()
 	end
+    | ("-I"|"-include" as o) :: s :: rem -> parse (cfiles,s::o::args) rem
 
 (* Options for coqtop : c) options with 1 argument and possibly more *)
 
-    | ("-I"|"-include" as o) :: rem ->
-	begin
-	  match rem with
-	  | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem'
-	  | s :: "-as" :: [] -> usage ()
-	  | s :: rem' -> parse (cfiles,s::o::args) rem'
-	  | []        -> usage ()
-	end
-    | "-R" :: s :: "-as" :: t :: rem ->	parse (cfiles,t::"-as"::s::"-R"::args) rem
-    | "-R" :: s :: "-as" :: [] -> usage ()
-    | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
-    | "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem
+    | ("-R"|"-Q" as o) :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
     | ("-schedule-vio-checking"
       |"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem ->
         let nodash, rem =
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index be50b0e1c7..13705edaaa 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -427,11 +427,28 @@ let coq_dependencies_dump chan dumpboxes =
 end
 
 let usage () =
-  eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] <filename>+\n";
-  eprintf " extra options:\n";
-  eprintf "  -coqlib dir : set the coq standard library directory\n";
-  eprintf "  -exclude-dir f : skip subdirectories named 'f' during -R search\n";
+  eprintf " usage: coqdep [options] <filename>+\n";
+  eprintf " options:\n";
+  eprintf "  -c : Also print the dependencies of caml modules (=ocamldep).\n";
+  (* Does not work anymore  *)
+  (* eprintf " -w : Print informations on missing or wrong \"Declare
+     ML Module\" commands in coq files.\n";  *)
+  (* Does not work anymore: *)
+  (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *)
+  eprintf "  -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n";
+  eprintf "  -sort : output the given file name ordered by dependencies\n";
+  eprintf "  -noglob | -no-glob : \n";
+  eprintf "  -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n";
+  eprintf "  -I dir : add (non recursively) dir to ocaml path\n";
+  eprintf "  -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *)
+  eprintf "  -R dir logname : add and import dir recursively to coq load path under logical name logname\n";
+  eprintf "  -Q dir logname : add (recusively) and open (non recursively) dir to coq load path under logical name logname\n";
   eprintf "  -dumpgraph f : print a dot dependency graph in file 'f'\n";
+  eprintf "  -dumpgraphbox f : print a dot dependency graph box in file 'f'\n";
+  eprintf "  -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n";
+  eprintf "  -coqlib dir : set the coq standard library directory\n";
+  eprintf "  -suffix s : \n";
+  eprintf "  -slash : deprecated, no effect\n";
   exit 1
 
 let split_period = Str.split (Str.regexp (Str.quote "."))
@@ -443,16 +460,10 @@ let rec parse = function
   | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
-  | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [];
-    add_dir add_known r (split_period ln);
-    parse ll
-  | "-I" :: r :: "-as" :: [] -> usage ()
   | "-I" :: r :: ll -> add_caml_dir r; parse ll
   | "-I" :: [] -> usage ()
-  | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
-  | "-R" :: r :: "-as" :: [] -> usage ()
-  | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
-  | "-Q" :: r :: ln :: ll -> add_dir add_known r (split_period ln); parse ll
+  | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
+  | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll
   | "-R" :: ([] | [_]) -> usage ()
   | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
   | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
@@ -472,24 +483,27 @@ let rec parse = function
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   parse (List.tl (Array.to_list Sys.argv));
+  (* Add current dir with empty logical path if not set by options above. *)
+  (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd()))
+   with Not_found -> add_norec_dir_import add_known "." []);
   if not Coq_config.has_natdynlink then option_natdynlk := false;
   (* NOTE: These directories are searched from last to first *)
   if !option_boot then begin
-    add_rec_dir add_known "theories" ["Coq"];
-    add_rec_dir add_known "plugins" ["Coq"];
+    add_rec_dir_import add_known "theories" ["Coq"];
+    add_rec_dir_import add_known "plugins" ["Coq"];
     add_caml_dir "tactics";
-    add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
-    add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
+    add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
+    add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
   end else begin
     Envars.set_coqlib ~fail:Errors.error;
     let coqlib = Envars.coqlib () in
-    add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
-    add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
+    add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
+    add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
-    if Sys.file_exists user then add_dir add_coqlib_known user [];
-    List.iter (fun s -> add_dir add_coqlib_known s [])
+    if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
+    List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
       (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x)));
-    List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath;
+    List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
   end;
   List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
   List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu;
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
new file mode 100644
index 0000000000..6fc826833e
--- /dev/null
+++ b/tools/coqdep_boot.ml
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Coqdep_common
+
+(** [coqdep_boot] is a stripped-down version of [coqdep], whose
+    behavior is the one of [coqdep -boot]. Its only dependencies
+    are [Coqdep_lexer], [Coqdep_common] and [Unix], and it should stay so.
+    If it needs someday some additional information, pass it via
+    options (see for instance [option_natdynlk] below).
+*)
+
+let rec parse = function
+  | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
+  | "-c" :: ll -> option_c := true; parse ll
+  | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
+  | "-mldep" :: ocamldep :: ll ->
+      option_mldep := Some ocamldep; option_c := true; parse ll
+  | "-I" :: r :: ll ->
+       (* To solve conflict (e.g. same filename in kernel and checker)
+          we allow to state an explicit order *)
+       add_caml_dir r;
+       norec_dirs := StrSet.add r !norec_dirs;
+       parse ll
+  | f :: ll -> treat_file None f; parse ll
+  | [] -> ()
+
+let _ =
+  let () = option_boot := true in
+  if Array.length Sys.argv < 2 then exit 1;
+  parse (List.tl (Array.to_list Sys.argv));
+  if !option_c then begin
+    add_rec_dir_import add_known "." [];
+    add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"];
+  end
+  else begin
+    add_rec_dir_import add_known "theories" ["Coq"];
+    add_rec_dir_import add_known "plugins" ["Coq"];
+    add_caml_dir "tactics";
+    add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
+    add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
+  end;
+  if !option_c then mL_dependencies ();
+  coq_dependencies ()
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 2cdb66aa74..c63e4aaa64 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -165,11 +165,6 @@ let warning_module_notfound f s =
   eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
     f (String.concat "." s)
 
-let warning_notfound f s =
-  eprintf "*** Warning: in file %s, the file " f;
-  eprintf "%s.v is required and has not been found!\n" s;
-  flush stderr
-
 let warning_declare f s =
   eprintf "*** Warning: in file %s, declared ML module " f;
   eprintf "%s has not been found!\n" s;
@@ -210,6 +205,18 @@ let absolute_file_name basename odir =
   let dir = match odir with Some dir -> dir | None -> "." in
   absolute_dir dir // basename
 
+(** [find_dir_logpath dir] Return the logical path of directory [dir]
+    if it has been given one. Raise [Not_found] otherwise. In
+    particular we can check if "." has been attributed a logical path
+    after processing all options and silently give the default one if
+    it hasn't. We may also use this to warn if ap hysical path is met
+    twice.*)
+let register_dir_logpath,find_dir_logpath =
+  let tbl: (string, string list) Hashtbl.t = Hashtbl.create 19 in
+  let reg physdir logpath = Hashtbl.add tbl (absolute_dir physdir) logpath in
+  let fnd physdir = Hashtbl.find tbl (absolute_dir physdir) in
+  reg,fnd
+
 let file_name s = function
   | None     -> s
   | Some "." -> s
@@ -329,7 +336,8 @@ let escape =
     Buffer.contents s'
 
 let compare_file f1 f2 =
-  absolute_dir (Filename.dirname f1) = absolute_dir (Filename.dirname f2)
+  absolute_file_name (Filename.basename f1) (Some (Filename.dirname f1))
+  = absolute_file_name (Filename.basename f2) (Some (Filename.dirname f2))
 
 let canonize f =
   let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
@@ -481,15 +489,15 @@ let add_caml_known phys_dir _ f =
     | _ -> ()
 
 let add_coqlib_known recur phys_dir log_dir f =
-  match get_extension f [".vo"] with
-    | (basename,".vo") ->
+  match get_extension f [".vo"; ".vio"] with
+    | (basename, (".vo" | ".vio")) ->
         let name = log_dir@[basename] in
         let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
 let add_known recur phys_dir log_dir f =
-  match get_extension f [".v";".vo"] with
+  match get_extension f [".v"; ".vo"; ".vio"] with
     | (basename,".v") ->
 	let name = log_dir@[basename] in
 	let file = phys_dir//basename in
@@ -498,7 +506,7 @@ let add_known recur phys_dir log_dir f =
           let paths = List.tl (suffixes name) in
           let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
           List.iter iter paths
-    | (basename,".vo") when not(!option_boot) ->
+    | (basename, (".vo" | ".vio")) when not(!option_boot) ->
         let name = log_dir@[basename] in
 	let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
@@ -509,11 +517,12 @@ let add_known recur phys_dir log_dir f =
 let is_not_seen_directory phys_f =
   not (StrSet.mem phys_f !norec_dirs)
 
-let rec add_directory add_file phys_dir log_dir =
+let rec add_directory recur add_file phys_dir log_dir =
+  register_dir_logpath phys_dir log_dir;
   let f = function
     | FileDir (phys_f,f) ->
-        if is_not_seen_directory phys_f then
-          add_directory add_file phys_f (log_dir @ [f])
+        if is_not_seen_directory phys_f && recur then
+          add_directory true add_file phys_f (log_dir @ [f])
     | FileRegular f ->
         add_file phys_dir log_dir f
   in
@@ -523,24 +532,29 @@ let rec add_directory add_file phys_dir log_dir =
   else
     warning_cannot_open_dir phys_dir
 
+(** Simply add this directory and imports it, no subdirs. This is used
+    by the implicit adding of the current path (which is not recursive). *)
+let add_norec_dir_import add_file phys_dir log_dir =
+  try add_directory false (add_file true) phys_dir log_dir with Unix_error _ -> ()
+
 (** -Q semantic: go in subdirs but only full logical paths are known. *)
-let add_dir add_file phys_dir log_dir =
-  try add_directory (add_file false) phys_dir log_dir with Unix_error _ -> ()
+let add_rec_dir_no_import add_file phys_dir log_dir =
+  try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> ()
 
 (** -R semantic: go in subdirs and suffixes of logical paths are known. *)
-let add_rec_dir add_file phys_dir log_dir =
-  add_directory (add_file true) phys_dir log_dir
+let add_rec_dir_import add_file phys_dir log_dir =
+  add_directory true (add_file true) phys_dir log_dir
 
 (** -R semantic but only on immediate capitalized subdirs *)
 
 let add_rec_uppercase_subdirs add_file phys_dir log_dir =
   process_subdirectories (fun phys_dir f ->
-    add_directory (add_file true) phys_dir (log_dir@[String.capitalize f]))
+    add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f]))
     phys_dir
 
 (** -I semantic: do not go in subdirs. *)
 let add_caml_dir phys_dir =
-  add_directory add_caml_known phys_dir []
+  add_directory false add_caml_known phys_dir []
 
 let rec treat_file old_dirname old_name =
   let name = Filename.basename old_name
@@ -555,15 +569,12 @@ let rec treat_file old_dirname old_name =
   match try (stat complete_name).st_kind with _ -> S_BLK with
     | S_DIR ->
 	(if name.[0] <> '.' then
-	   let dir=opendir complete_name in
            let newdirname =
              match dirname with
                | None -> name
                | Some d -> d//name
 	   in
-	   try
-	     while true do treat_file (Some newdirname) (readdir dir) done
-	   with End_of_file -> closedir dir)
+           Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
     | S_REG ->
 	(match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
 	   | (base,".v") ->
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index c3570f811b..633c474ada 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,6 +8,14 @@
 
 module StrSet : Set.S with type elt = string
 
+(** [find_dir_logpath dir] Return the logical path of directory [dir]
+    if it has been given one. Raise [Not_found] otherwise. In
+    particular we can check if "." has been attributed a logical path
+    after processing all options and silently give the default one if
+    it hasn't. We may also use this to warn if ap hysical path is met
+    twice.*)
+val find_dir_logpath: string -> string list
+
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
@@ -42,11 +50,22 @@ val add_known : bool -> string -> string list -> string -> unit
 val add_coqlib_known : bool -> string -> string list -> string -> unit
 val add_caml_known : string -> string list -> string -> unit
 val add_caml_dir : string -> unit
-val add_dir :
+
+(** Simply add this directory and imports it, no subdirs. This is used
+    by the implicit adding of the current path. *)
+val add_norec_dir_import :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-val add_rec_dir :
+
+(** -Q semantic: go in subdirs but only full logical paths are known. *)
+val add_rec_dir_no_import :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
+(** -R semantic: go in subdirs and suffixes of logical paths are known. *)
+val add_rec_dir_import :
+  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
 val add_rec_uppercase_subdirs :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
 val treat_file : dir -> string -> unit
 val error_cannot_parse : string -> int * int -> 'a
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index 84c9ba798b..bb17fdf9f4 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 291bc55fbe..eb233b8f94 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -25,13 +25,6 @@
   exception Fin_fichier
   exception Syntax_error of int*int
 
-  let module_current_name = ref []
-  let module_names = ref []
-  let ml_module_name = ref ""
-  let loadpath = ref ""
-
-  let mllist = ref ([] : string list)
-
   let field_name s = String.sub s 1 (String.length s - 1)
 
   let unquote_string s =
@@ -46,11 +39,6 @@
 
   let syntax_error lexbuf =
     raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
-
-  (** This is the prefix that should be pre-prepended to files due to the use
-   ** of [From], i.e. [From Xxx... Require ...]
-   **)
-  let from_pre_ident = ref None
 }
 
 let space = [' ' '\t' '\n' '\r']
@@ -81,9 +69,9 @@ let dot = '.' ( space+ | eof)
 
 rule coq_action = parse
   | "Require" space+
-      { require_modifiers lexbuf }
+      { require_modifiers None lexbuf }
   | "Local"? "Declare" space+ "ML" space+ "Module" space+
-      { mllist := []; modules lexbuf }
+      { modules [] lexbuf }
   | "Load" space+
       { load_file lexbuf }
   | "Add" space+ "LoadPath" space+
@@ -109,38 +97,34 @@ and from_rule = parse
   | space+
       { from_rule lexbuf }
   | coq_ident
-      { module_current_name := [Lexing.lexeme lexbuf];
-	from_pre_ident := Some (coq_qual_id_tail lexbuf);
-	module_names := [];
-	consume_require lexbuf }
+      { let from = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+        consume_require (Some from) lexbuf }
   | eof
       { syntax_error lexbuf }
   | _
       { syntax_error lexbuf }
 
-and require_modifiers = parse
+and require_modifiers from = parse
   | "(*"
-      { comment lexbuf; require_modifiers lexbuf }
+      { comment lexbuf; require_modifiers from lexbuf }
   | "Import" space+
-      { require_file lexbuf }
+      { require_file from lexbuf }
   | "Export" space+
-      { require_file lexbuf }
+      { require_file from lexbuf }
   | space+
-      { require_modifiers lexbuf }
+      { require_modifiers from lexbuf }
   | eof
       { syntax_error lexbuf }
   | _
-      { backtrack lexbuf ; require_file lexbuf }
+      { backtrack lexbuf ; require_file from lexbuf }
 
-and consume_require = parse
+and consume_require from = parse
   | "(*"
-      { comment lexbuf; consume_require lexbuf }
+      { comment lexbuf; consume_require from lexbuf }
   | space+
-      { consume_require lexbuf }
+      { consume_require from lexbuf }
   | "Require" space+
-      { require_modifiers lexbuf }
-  | eof
-      { syntax_error lexbuf }
+      { require_modifiers from lexbuf }
   | _
       { syntax_error lexbuf }
 
@@ -152,20 +136,19 @@ and add_loadpath = parse
   | eof
       { syntax_error lexbuf }
   | '"' [^ '"']* '"' (*'"'*)
-      { loadpath := unquote_string (lexeme lexbuf);
-        add_loadpath_as lexbuf }
+      { add_loadpath_as (unquote_string (lexeme lexbuf)) lexbuf }
 
-and add_loadpath_as = parse
+and add_loadpath_as path = parse
   | "(*"
-      { comment lexbuf; add_loadpath_as lexbuf }
+      { comment lexbuf; add_loadpath_as path lexbuf }
   | space+
-      { add_loadpath_as lexbuf }
+      { add_loadpath_as path lexbuf }
   | "as"
       { let qid = coq_qual_id lexbuf in
         skip_to_dot lexbuf;
-        AddRecLoadPath (!loadpath,qid) }
+        AddRecLoadPath (path, qid) }
   | dot
-      { AddLoadPath !loadpath }
+      { AddLoadPath path }
 
 and caml_action = parse
   | space +
@@ -176,8 +159,7 @@ and caml_action = parse
         { caml_action lexbuf }
   | caml_low_ident { caml_action lexbuf }
   | caml_up_ident
-      { ml_module_name := Lexing.lexeme lexbuf;
-        qual_id lexbuf }
+      { qual_id (Lexing.lexeme lexbuf) lexbuf }
   | ['0'-'9']+
     | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
     | '0' ['o' 'O'] ['0'-'7']+
@@ -260,18 +242,15 @@ and load_file = parse
   | _
       { syntax_error lexbuf }
 
-and require_file = parse
+and require_file from = parse
   | "(*"
-      { comment lexbuf; require_file lexbuf }
+      { comment lexbuf; require_file from lexbuf }
   | space+
-      { require_file lexbuf }
+      { require_file from lexbuf }
   | coq_ident
-      { module_current_name := [Lexing.lexeme lexbuf];
-        module_names := [coq_qual_id_tail lexbuf];
-        let qid = coq_qual_id_list lexbuf in
+      { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+        let qid = coq_qual_id_list [name] lexbuf in
         parse_dot lexbuf;
-        let from = !from_pre_ident in
-        from_pre_ident := None;
         Require (from, qid) }
   | eof
       { syntax_error lexbuf }
@@ -294,66 +273,55 @@ and coq_qual_id = parse
   | space+
       { coq_qual_id lexbuf }
   | coq_ident
-      { module_current_name := [Lexing.lexeme lexbuf];
-        coq_qual_id_tail lexbuf }
-  | eof
-      { syntax_error lexbuf }
+      { coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf }
   | _
-      { backtrack lexbuf;
-        let qid = List.rev !module_current_name in
-        module_current_name := [];
-        qid }
+      { syntax_error lexbuf }
 
-and coq_qual_id_tail = parse
+and coq_qual_id_tail module_name = parse
   | "(*"
-      { comment lexbuf; coq_qual_id_tail lexbuf }
+      { comment lexbuf; coq_qual_id_tail module_name lexbuf }
   | space+
-      { coq_qual_id_tail lexbuf }
+      { coq_qual_id_tail module_name lexbuf }
   | coq_field
-      { module_current_name :=
-          field_name (Lexing.lexeme lexbuf) :: !module_current_name;
-        coq_qual_id_tail lexbuf }
+      { coq_qual_id_tail (field_name (Lexing.lexeme lexbuf) :: module_name) lexbuf }
   | eof
       { syntax_error lexbuf }
   | _
       { backtrack lexbuf;
-        let qid = List.rev !module_current_name in
-        module_current_name := [];
-        qid }
+        List.rev module_name }
 
-and coq_qual_id_list = parse
+and coq_qual_id_list module_names = parse
   | "(*"
-      { comment lexbuf; coq_qual_id_list lexbuf }
+      { comment lexbuf; coq_qual_id_list module_names lexbuf }
   | space+
-      { coq_qual_id_list lexbuf }
+      { coq_qual_id_list module_names lexbuf }
   | coq_ident
-      { module_current_name := [Lexing.lexeme lexbuf];
-        module_names := coq_qual_id_tail lexbuf :: !module_names;
-        coq_qual_id_list lexbuf
+      { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+        coq_qual_id_list (name :: module_names) lexbuf
       }
   | eof
       { syntax_error lexbuf }
   | _
       { backtrack lexbuf;
-        List.rev !module_names }
+        List.rev module_names }
 
-and modules = parse
+and modules mllist = parse
   | space+
-      { modules lexbuf }
+      { modules mllist lexbuf }
   | "(*"
-      { comment lexbuf; modules lexbuf }
+      { comment lexbuf; modules mllist lexbuf }
   | '"' [^'"']* '"'
       { let lex = (Lexing.lexeme lexbuf) in
 	let str = String.sub lex 1 (String.length lex - 2) in
-	mllist := str :: !mllist; modules lexbuf}
+        modules (str :: mllist) lexbuf}
   | eof
       { syntax_error lexbuf }
   | _
-      { (Declare (List.rev !mllist)) }
+      { Declare (List.rev mllist) }
 
-and qual_id = parse
-  | '.' [^ '.' '(' '['] {
-      Use_module (String.uncapitalize !ml_module_name) }
+and qual_id ml_module_name = parse
+  | '.' [^ '.' '(' '[']
+      { Use_module (String.uncapitalize ml_module_name) }
   | eof { raise Fin_fichier }
   | _ { caml_action lexbuf }
 
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index c3db3a265d..f817ed5a2a 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 46005741da..f6d47a55de 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index de7290a440..5d48473d8c 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 4e132ba03d..58b19184e7 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index cb70414675..431080c6bc 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -320,6 +320,7 @@ let def_token =
   | "Instance"
   | "Declare" space+ "Instance"
   | "Global" space+ "Instance"
+  | "Functional" space+ "Scheme"
 
 let decl_token =
   "Hypothesis"
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 4a5ff59245..47acc7b436 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 69b4e4daea..e44bbd593a 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2554ed495b..fe4387381d 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -61,8 +61,8 @@ let usage () =
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
   prerr_endline "  -Q <dir> <coqdir>    map physical dir to Coq dir";
-  prerr_endline "  --latin1             set ISO-8859-1 input language";
-  prerr_endline "  --utf8               set UTF-8 input language";
+  prerr_endline "  --latin1             set ISO-8859-1 mode";
+  prerr_endline "  --utf8               set UTF-8 mode";
   prerr_endline "  --charset <string>   set HTML charset";
   prerr_endline "  --inputenc <string>  set LaTeX input encoding";
   prerr_endline "  --interpolate        try to typeset identifiers in comments using definitions in the same module";
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 06030c45a6..2b2690968d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -197,8 +197,11 @@ module Latex = struct
     printf "\n";
     printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
     printf "%%interpret utf8 characters but extra packages might have to be added\n";
-    printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
-    printf "%%Use coqdoc's option -p to add new packages.\n";
+    printf "%%such as \"textgreek\" for Greek letters not already in tipa\n";
+    printf "%%or \"stmaryrd\" for mathematical symbols.\n";
+    printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n";
+    printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n";
+    printf "%%Use coqdoc's option -p to add new packages or declarations.\n";
     printf "\\usepackage{tipa}\n";
     printf "\n"
 
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index c4628dd846..853bc29aa4 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index a93ae85579..b6a1057aa8 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index c4fe3bc8f3..f07efedf9e 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index a6254b2a44..6f3d8e2b8f 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -279,7 +279,7 @@ let main () =
     (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
        - With the coq .cma, we MUST use the -linkall option. *)
     let args =
-      "-linkall" :: "-rectypes" :: flags @ copts @ options @
+      "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @
       (std_includes basedir) @ tolink @ [ main_file ] @ topstart
     in
     if !echo then begin
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 9a42553da2..b4fc738d0e 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index 8c08915054..d7bdf907a2 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index a9a7251c51..e81f4038d6 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -17,7 +17,18 @@ type coqtop = {
   xml_parser : Xml_parser.t;
 }
 
-let logger level content = prerr_endline content
+let print_xml chan xml =
+  let rec print = function
+  | Xml_datatype.PCData s -> output_string chan s
+  | Xml_datatype.Element (_, _, children) -> List.iter print children
+  in
+  print xml
+
+let error_xml s =
+  Printf.eprintf "fake_id: error: %a\n%!" print_xml s;
+  exit 1
+
+let logger level content = Printf.eprintf "%a\n%! " print_xml content
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -38,8 +49,8 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   let res = loop () in
   if print then prerr_endline (Xmlprotocol.pr_full_value call res);
   match res with
-  | Interface.Fail (_,_,s) when fail -> error s
-  | Interface.Fail (_,_,s) as x -> prerr_endline s; x
+  | Interface.Fail (_,_,s) when fail -> error_xml (Richpp.repr s)
+  | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml (Richpp.repr s); x
   | x -> x
 
 let eval_call c q = ignore(base_eval_call c q)
@@ -188,7 +199,7 @@ let print_document () =
 module GUILogic = struct
 
   let after_add = function
-    | Interface.Fail (_,_,s) -> error s
+    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
     | Interface.Good (id, (Util.Inl (), _)) ->
         Document.assign_tip_id doc id
     | Interface.Good (id, (Util.Inr tip, _)) ->
@@ -200,7 +211,7 @@ module GUILogic = struct
   let at id id' _ = Stateid.equal id' id
   
   let after_edit_at (id,need_unfocus) = function
-    | Interface.Fail (_,_,s) -> error s
+    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
     | Interface.Good (Util.Inl ()) ->
         if need_unfocus then Document.unfocus doc;
         ignore(Document.cut_at doc id);
@@ -323,7 +334,7 @@ let main =
   let finish () =
     match base_eval_call (Xmlprotocol.status true) coq with
     | Interface.Good _ -> exit 0
-    | Interface.Fail (_,_,s) -> error s in
+    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) in
   (* The main loop *)
   init ();
   while true do
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 5ce19e7f88..0bf98a8f0f 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 9dd49b90ad..449efd57cd 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 4e5edcf6c2..670ff487c5 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -98,23 +98,14 @@ let file_name s = function
 
 type dir = string option
 
-(* Visits all the directories under [dir], including [dir],
-   or just [dir] if [recur=false] *)
-
-let rec add_directory add_file phys_dir =
-  let dirh = opendir phys_dir in
-  try
-    while true do
-      let f = readdir dirh in
-      (* we avoid all files and subdirs starting by '.' (e.g. .svn),
-         plus CVS and _darcs and any subdirs given via -exclude-dirs *)
-      if f.[0] <> '.' then
-        let phys_f = if phys_dir = "." then f else phys_dir//f in
-	match try (stat phys_f).st_kind with _ -> S_BLK with
-	  | S_REG -> add_file phys_dir f
-	  | _ -> ()
-    done
-  with End_of_file -> closedir dirh
+let add_directory add_file phys_dir =
+  Array.iter (fun f ->
+    (* we avoid all files starting by '.' *)
+    if f.[0] <> '.' then
+      let phys_f = if phys_dir = "." then f else phys_dir//f in
+      match try (stat phys_f).st_kind with _ -> S_BLK with
+      | S_REG -> add_file phys_dir f
+      | _ -> ()) (Sys.readdir phys_dir)
 
 let error_cannot_parse s (i,j) =
   Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
@@ -173,7 +164,7 @@ let traite_fichier_modules md ext =
 
 let addQueue q v = q := v :: !q
 
-let rec treat_file old_name =
+let treat_file old_name =
   let name = Filename.basename old_name in
   let dirname = Some (Filename.dirname old_name) in
   match get_extension name [".mllib"] with