28 files changed, 79 insertions, 62 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index bd9d8c9221..d37d2bea94 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -38,6 +38,7 @@ DOCDIR            := $(COQMF_DOCDIR)
 OCAMLFIND         := $(COQMF_OCAMLFIND)
 CAMLFLAGS         := $(COQMF_CAMLFLAGS)
 HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
+OCAMLWARN         := $(COQMF_WARN)
 
 @CONF_FILE@: @PROJECT_FILE@
 	@COQ_MAKEFILE_INVOCATION@
@@ -170,13 +171,13 @@ DYNOBJ:=.cmxs
 DYNLIB:=.cmxs
 endif
 
-# these variables are meant to be overriden if you want to add *extra* flags
+# these variables are meant to be overridden if you want to add *extra* flags
 COQEXTRAFLAGS?=
 COQCHKEXTRAFLAGS?=
 COQDOCEXTRAFLAGS?=
 
 # these flags do NOT contain the libraries, to make them easier to overwrite
-COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS)
+COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS)
 COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
 COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS)
 
@@ -190,9 +191,9 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@
 COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 
 CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
-
 # ocamldoc fails with unknown argument otherwise
-CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLFLAGS+=$(OCAMLWARN)
 
 ifneq (,$(TIMING))
 TIMING_ARG=-time
@@ -468,6 +469,9 @@ beautify: $(BEAUTYFILES)
 # Extensions can't assume when they run.
 
 install:
+	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
+	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
+	done; exit $$code
 	$(HIDE)for f in $(FILESTOINSTALL); do\
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
 	 if [ "$$?" != "0" -o -z "$$df" ]; then\
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index fa8b771a74..adb416e3ce 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -128,6 +128,7 @@ module Options = struct
   [ { enabled = false; cmd = "-debug"; }
   ; { enabled = false; cmd = "-native_compiler"; }
   ; { enabled = true; cmd = "-allow-sprop"; }
+  ; { enabled = true; cmd = "-w +default"; }
   ]
 
   let build_coq_flags () =
@@ -192,9 +193,7 @@ let pp_vo_dep dir fmt vo =
   pp_rule fmt all_targets deps action
 
 let pp_mlg_dep _dir fmt ml =
-  let target = Filename.(remove_extension ml) ^ ".ml" in
-  let mlg_rule = "(run coqpp %{pp-file})" in
-  pp_rule fmt [target] [ml] mlg_rule
+  fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml)
 
 let pp_dep dir fmt oo = match oo with
   | VO vo -> pp_vo_dep dir fmt vo
@@ -214,7 +213,7 @@ let record_dune d ff =
   if Sys.file_exists sd && Sys.is_directory sd then
     let out = open_out (bpath [sd;"dune"]) in
     let fmt = formatter_of_out_channel out in
-    if List.nth d 0 = "plugins" then
+    if List.nth d 0 = "plugins" || List.nth d 0 = "user-contrib" then
       fprintf fmt "(include plugin_base.dune)@\n";
     out_install fmt d ff;
     List.iter (pp_dep d fmt) ff;
@@ -224,17 +223,20 @@ let record_dune d ff =
     eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd
 
 (* File Scanning *)
-let scan_mlg m d =
-  let dir = ["plugins"; d] in
+let scan_mlg ~root m d =
+  let dir = [root; d] in
   let m = DirMap.add dir [] m in
   let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg"))
                    Array.(to_list @@ readdir (bpath dir))) in
-  List.fold_left (fun m f -> add_map_list ["plugins"; d] (MLG f) m) m mlg
+  List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg
 
-let scan_plugins m =
+let scan_dir ~root m =
   let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in
-  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in
-  List.fold_left scan_mlg m dirs
+  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in
+  List.fold_left (scan_mlg ~root) m dirs
+
+let scan_plugins m = scan_dir ~root:"plugins" m
+let scan_usercontrib m = scan_dir ~root:"user-contrib" m
 
 (* This will be removed when we drop support for Make *)
 let fix_cmo_cma file =
@@ -291,5 +293,6 @@ let exec_ifile f =
 let _ =
   exec_ifile (fun ic ->
       let map = scan_plugins DirMap.empty in
+      let map = scan_usercontrib map in
       let map = read_vfiles ic map in
       out_map map)
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 68281d6481..1bd52d5bf1 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index c6d3551561..371483b862 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 66f1f257b8..6f81be475b 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -297,7 +297,7 @@ module DAG = DAG(struct type t = string let compare = compare end)
 (** TODO: we should share this code with Coqdep_common *)
 module VData = struct
   type t = string list option * string list
-  let compare = Pervasives.compare
+  let compare = Util.pervasives_compare
 end
 
 module VCache = Set.Make(VData)
@@ -454,7 +454,7 @@ let usage () =
   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 "  -Q dir logname : add (recursively) 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";
@@ -529,6 +529,11 @@ let coqdep () =
     add_rec_dir_import add_known "plugins" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
+    let user = "user-contrib" in
+    if Sys.file_exists user then begin
+      add_rec_dir_no_import add_known user [];
+      add_rec_dir_no_import (fun _ -> add_caml_known) user [];
+    end;
   end else begin
     (* option_boot is actually always false in this branch *)
     Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
@@ -563,4 +568,5 @@ let _ =
   try
     coqdep ()
   with CoqlibError msg ->
-    eprintf "*** Error: %s@\n%!" msg
+    eprintf "*** Error: %s@\n%!" msg;
+    exit 1
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index aa023e6986..1730dd3d68 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -17,6 +17,9 @@ open Coqdep_common
     options (see for instance [option_natdynlk] below).
 *)
 
+let split_period = Str.split (Str.regexp (Str.quote "."))
+let add_q_include path l = add_rec_dir_no_import add_known path (split_period l)
+
 let rec parse = function
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
   | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
@@ -33,6 +36,7 @@ let rec parse = function
        add_caml_dir r;
        norec_dirs := StrSet.add r !norec_dirs;
        parse ll
+  | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index e3dd32fb63..8beb314046 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -357,7 +357,7 @@ let canonize f =
 
 module VData = struct
   type t = string list option * string list
-  let compare = Pervasives.compare
+  let compare = compare
 end
 
 module VCache = Set.Make(VData)
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 91d2b45876..e450d0e36f 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index 0e2b332f1e..018fc1b7a2 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 5533ab106d..743da535b8 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 36ce405fe6..4def233ff8 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 863034504c..c74df82d4b 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5dd6cc6c83..dc13acadcb 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 7732610f5c..dcc1369c72 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 230c5524b7..a44ddf7467 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -940,7 +940,7 @@ and escaped_coq = parse
       { (* likely to be a syntax error: we escape *) backtrack lexbuf }
   | eof
       { Tokens.flush_sublexer () }
-  | (identifier '.')* identifier
+  | identifier
       { Tokens.flush_sublexer();
         Output.ident (lexeme lexbuf) None;
         escaped_coq lexbuf }
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 8d395b418f..8f82bee5c6 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 7c9aad67fc..c05b2a459a 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 11ec3d3993..3442ebb731 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -396,7 +396,7 @@ let copy src dst =
   try
     let cout = open_out dst in
     try
-      while true do Pervasives.output_char cout (input_char cin) done
+      while true do output_char cout (input_char cin) done
     with End_of_file ->
       close_out cout;
       close_in cin
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index b703af934d..02f0290802 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -13,9 +13,9 @@ open Index
 
 (*s Low level output *)
 
-let output_char c = Pervasives.output_char !out_channel c
+let output_char c = output_char !out_channel c
 
-let output_string s = Pervasives.output_string !out_channel s
+let output_string s = output_string !out_channel s
 
 let printf s = Printf.fprintf !out_channel s
 
@@ -527,13 +527,13 @@ module Html = struct
   let header () =
     if !header_trailer then
       if !header_file_spec then
-	let cin = Pervasives.open_in !header_file in
+        let cin = open_in !header_file in
 	  try
 	    while true do
-	      let s = Pervasives.input_line cin in
+              let s = input_line cin in
 		printf "%s\n" s
 	    done
-	  with End_of_file -> Pervasives.close_in cin
+          with End_of_file -> close_in cin
       else
 	begin
 	  printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
@@ -548,13 +548,13 @@ module Html = struct
 
   let trailer () =
     if !header_trailer && !footer_file_spec then
-	let cin = Pervasives.open_in !footer_file in
+        let cin = open_in !footer_file in
 	  try
 	    while true do
-	      let s = Pervasives.input_line cin in
+              let s = input_line cin in
 		printf "%s\n" s
 	    done
-	  with End_of_file -> Pervasives.close_in cin
+          with End_of_file -> close_in cin
     else
       begin
         if !index && (get_module false) <> "Index" then
@@ -762,7 +762,7 @@ module Html = struct
 
   (* inference rules *)
   let inf_rule assumptions (_,_,midnm) conclusions =
-    (* this first function replaces any occurance of 3 or more spaces
+    (* this first function replaces any occurrence of 3 or more spaces
        in a row with "&nbsp;"s.  We do this to the assumptions so that
        people can put multiple rules on a line with nice formatting *)
     let replace_spaces str =
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index a8a50d751d..ceed67fff2 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 49f7ef2f5d..5adc18e1a0 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index 00db2ad317..1ec541f417 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -57,7 +57,7 @@ val translate : string -> string option
      dictionary, "<>_h" is one word and gets translated
 *)
 
-(* Warning: do not output anything on output channel inbetween a call
+(* Warning: do not output anything on output channel in between a call
    to [output_tagged_*] and [flush_sublexer]!! *)
 
 type out_function =
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index f0f138740c..cfd65a2349 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -207,7 +207,7 @@ and string = parse
   | eof  { 0 }
 
 (*s The following entry [read_header] is used to skip the possible header at
-    the beggining of files (unless option \texttt{-e} is specified).
+    the beginning of files (unless option \texttt{-e} is specified).
     It stops whenever it encounters an empty line or any character outside
     a comment. In this last case, it correctly resets the lexer position
     on that character (decreasing [lex_curr_pos] by 1). *)
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index bfea141bb3..9f9c6dd5d0 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py
index 32c52c7a17..fddf75f39f 100755
--- a/tools/make-both-single-timing-files.py
+++ b/tools/make-both-single-timing-files.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 import sys
 from TimeFileMaker import *
 
diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py
index f730a8d6bd..8937d63c2f 100755
--- a/tools/make-both-time-files.py
+++ b/tools/make-both-time-files.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 import sys
 from TimeFileMaker import *
 
diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py
index e66136df9d..ad0a04ab07 100755
--- a/tools/make-one-time-file.py
+++ b/tools/make-one-time-file.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 import sys
 from TimeFileMaker import *
 
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 680c8f30ae..41a4e2a86a 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -35,7 +35,6 @@ rule mllib_list = parse
 
 {
 open Printf
-open Unix
 
 (* Makefile's escaping rules are awful: $ is escaped by doubling and
    other special characters are escaped by backslash prefixing while
@@ -99,6 +98,7 @@ let file_name s = function
 type dir = string option
 
 let add_directory add_file phys_dir =
+  let open Unix in
   Array.iter (fun f ->
     (* we avoid all files starting by '.' *)
     if f.[0] <> '.' then
@@ -152,7 +152,7 @@ let add_caml_known phys_dir f =
     | _ -> ()
 
 let add_caml_dir phys_dir =
-  handle_unix_error (add_directory add_caml_known) phys_dir
+  Unix.handle_unix_error (add_directory add_caml_known) phys_dir
 
 let traite_fichier_modules md ext =
   try
@@ -192,7 +192,7 @@ let mllib_dependencies () =
          efullname efullname;
        printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n"
          efullname efullname;
-       flush Pervasives.stdout)
+       flush stdout)
     (List.rev !mllibAccu)
 
 let mlpack_dependencies () =
@@ -209,7 +209,7 @@ let mlpack_dependencies () =
          efullname efullname;
        printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n"
          efullname efullname;
-       flush Pervasives.stdout)
+       flush stdout)
     (List.rev !mlpackAccu)
 
 let rec parse = function