Imported Upstream version 8.8.2upstream/8.8.2

40 files changed, 1958 insertions, 1507 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
new file mode 100644
index 00000000..f7e30eae
--- /dev/null
+++ b/tools/CoqMakefile.in
@@ -0,0 +1,799 @@
+###############################################################################
+##  v      #                   The Coq Proof Assistant                       ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                   ##
+##   \VV/  #                                                                 ##
+##    //   #                                                                 ##
+###############################################################################
+## GNUMakefile for Coq @COQ_VERSION@
+
+# For debugging purposes (must stay here, don't move below)
+INITIAL_VARS := $(.VARIABLES)
+# To implement recursion we save the name of the main Makefile
+SELF := $(lastword $(MAKEFILE_LIST))
+PARENT := $(firstword $(MAKEFILE_LIST))
+
+# This file is generated by coq_makefile and contains many variable
+# definitions, like the list of .v files or the path to Coq
+include @CONF_FILE@
+
+# Put in place old names
+VFILES            := $(COQMF_VFILES)
+MLIFILES          := $(COQMF_MLIFILES)
+MLFILES           := $(COQMF_MLFILES)
+ML4FILES          := $(COQMF_ML4FILES)
+MLPACKFILES       := $(COQMF_MLPACKFILES)
+MLLIBFILES        := $(COQMF_MLLIBFILES)
+CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
+INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
+OTHERFLAGS        := $(COQMF_OTHERFLAGS)
+COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
+OCAMLLIBS         := $(COQMF_OCAMLLIBS)
+SRC_SUBDIRS       := $(COQMF_SRC_SUBDIRS)
+COQLIBS           := $(COQMF_COQLIBS)
+COQLIBS_NOML      := $(COQMF_COQLIBS_NOML)
+CMDLINE_COQLIBS   := $(COQMF_CMDLINE_COQLIBS)
+LOCAL             := $(COQMF_LOCAL)
+COQLIB            := $(COQMF_COQLIB)
+DOCDIR            := $(COQMF_DOCDIR)
+OCAMLFIND         := $(COQMF_OCAMLFIND)
+CAMLP5O           := $(COQMF_CAMLP5O)
+CAMLP5BIN         := $(COQMF_CAMLP5BIN)
+CAMLP5LIB         := $(COQMF_CAMLP5LIB)
+CAMLP5OPTIONS     := $(COQMF_CAMLP5OPTIONS)
+CAMLFLAGS         := $(COQMF_CAMLFLAGS)
+HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
+
+@CONF_FILE@: @PROJECT_FILE@
+	@COQ_MAKEFILE_INVOCATION@
+
+# This file can be created by the user to hook into double colon rules or
+# add any other Makefile code he may need
+-include @LOCAL_FILE@
+
+# Parameters ##################################################################
+#
+# Parameters are make variable assignments.
+# They can be passed to (each call to) make on the command line.
+# They can also be put in @LOCAL_FILE@ once an for all.
+# For retro-compatibility reasons they can be put in the _CoqProject, but this
+# practice is discouraged since _CoqProject better not contain make specific
+# code (be nice to user interfaces).
+
+# Print shell commands (set to non empty)
+VERBOSE ?=
+
+# Time the Coq process (set to non empty), and how (see default value)
+TIMED?=
+TIMECMD?=
+# Use command time on linux, gtime on Mac OS
+TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+ifneq (,$(TIMED))
+ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=command time -f $(TIMEFMT)
+else
+ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=gtime -f $(TIMEFMT)
+else
+STDTIME?=command time
+endif
+endif
+else
+STDTIME?=command time -f $(TIMEFMT)
+endif
+
+# Coq binaries
+COQC     ?= "$(COQBIN)coqc"
+COQTOP   ?= "$(COQBIN)coqtop"
+COQCHK   ?= "$(COQBIN)coqchk"
+COQDEP   ?= "$(COQBIN)coqdep"
+GALLINA  ?= "$(COQBIN)gallina"
+COQDOC   ?= "$(COQBIN)coqdoc"
+COQMKFILE ?= "$(COQBIN)coq_makefile"
+
+# Timing scripts
+COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
+COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
+BEFORE ?=
+AFTER ?=
+
+# FIXME this should be generated by Coq (modules already linked by Coq)
+CAMLDONTLINK=camlp5.gramlib,unix,str
+
+# OCaml binaries
+CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
+CAMLOPTC    ?= "$(OCAMLFIND)" opt      -c
+CAMLLINK    ?= "$(OCAMLFIND)" ocamlc   -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLOPTLINK ?= "$(OCAMLFIND)" opt      -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLDOC     ?= "$(OCAMLFIND)" ocamldoc
+CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
+
+# DESTDIR is prepended to all installation paths
+DESTDIR ?=
+
+# Debug builds, typically -g to OCaml, -debug to Coq.
+CAMLDEBUG ?=
+COQDEBUG ?=
+
+# Extra packages to be linked in (as in findlib -package)
+CAMLPKGS ?=
+
+# Option for making timing files
+TIMING?=
+# Option for changing sorting of timing output file
+TIMING_SORT_BY ?= auto
+# Output file names for timed builds
+TIME_OF_BUILD_FILE               ?= time-of-build.log
+TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
+TIME_OF_BUILD_AFTER_FILE         ?= time-of-build-after.log
+TIME_OF_PRETTY_BUILD_FILE        ?= time-of-build-pretty.log
+TIME_OF_PRETTY_BOTH_BUILD_FILE   ?= time-of-build-both.log
+TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
+
+########## End of parameters ##################################################
+# What follows may be relevant to you only if you need to
+# extend this Makefile.  If so, look for 'Extension point' here and
+# put in @LOCAL_FILE@ double colon rules accordingly.
+# E.g. to perform some work after the all target completes you can write
+#
+# post-all::
+# 	echo "All done!"
+#
+# in @LOCAL_FILE@
+#
+###############################################################################
+
+
+
+
+# Flags #######################################################################
+#
+# We define a bunch of variables combining the parameters
+
+SHOW := $(if $(VERBOSE),@true "",@echo "")
+HIDE := $(if $(VERBOSE),,@)
+
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
+
+OPT?=
+
+# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
+ifeq '$(OPT)' '-byte'
+USEBYTE:=true
+DYNOBJ:=.cma
+DYNLIB:=.cma
+else
+USEBYTE:=
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
+endif
+
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
+COQCHKFLAGS?=-silent -o $(COQLIBS)
+COQDOCFLAGS?=-interpolate -utf8
+COQDOCLIBS?=$(COQLIBS_NOML)
+
+# The version of Coq being run and the version of coq_makefile that
+# generated this makefile
+COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
+COQMAKEFILE_VERSION:=@COQ_VERSION@
+
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
+
+CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB)
+
+# ocamldoc fails with unknown argument otherwise
+CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+
+# FIXME This should be generated by Coq
+GRAMMARS:=grammar.cma
+CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
+
+CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null)
+ifeq (,$(CAMLLIB))
+PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.")
+else
+PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl'
+endif
+
+ifneq (,$(TIMING))
+TIMING_ARG=-time
+ifeq (after,$(TIMING))
+TIMING_EXT=after-timing
+else
+ifeq (before,$(TIMING))
+TIMING_EXT=before-timing
+else
+TIMING_EXT=timing
+endif
+endif
+else
+TIMING_ARG=
+endif
+
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
+endif
+
+concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
+
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop)
+
+# Files #######################################################################
+#
+# We here define a bunch of variables about the files being part of the
+# Coq project in order to ease the writing of build target and build rules
+
+VDFILE := .coqdeps
+
+ALLSRCFILES := \
+	$(ML4FILES) \
+	$(MLFILES) \
+	$(MLPACKFILES) \
+	$(MLLIBFILES) \
+	$(MLIFILES)
+
+# helpers
+vo_to_obj = $(addsuffix .o,\
+  $(filter-out Warning: Error:,\
+  $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1))))
+strip_dotslash = $(patsubst ./%,%,$(1))
+VO = vo
+
+VOFILES = $(VFILES:.v=.$(VO))
+GLOBFILES = $(VFILES:.v=.glob)
+GFILES = $(VFILES:.v=.g)
+HTMLFILES = $(VFILES:.v=.html)
+GHTMLFILES = $(VFILES:.v=.g.html)
+BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
+TEXFILES = $(VFILES:.v=.tex)
+GTEXFILES = $(VFILES:.v=.g.tex)
+CMOFILES = \
+	$(ML4FILES:.ml4=.cmo) \
+	$(MLFILES:.ml=.cmo) \
+	$(MLPACKFILES:.mlpack=.cmo)
+CMXFILES = $(CMOFILES:.cmo=.cmx)
+OFILES = $(CMXFILES:.cmx=.o)
+CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma)
+CMXAFILES = $(CMAFILES:.cma=.cmxa)
+CMIFILES = \
+	$(CMOFILES:.cmo=.cmi) \
+	$(MLIFILES:.mli=.cmi)
+# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
+# a .ml4 file
+CMXSFILES = \
+	$(MLPACKFILES:.mlpack=.cmxs) \
+	$(CMXAFILES:.cmxa=.cmxs) \
+	$(if $(MLPACKFILES)$(CMXAFILES),,\
+		$(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs))
+
+# files that are packed into a plugin (no extension)
+PACKEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+            $(call strip_dotslash, \
+	       $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib))))
+# files that are archived into a .cma (mllib)
+LIBEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+            $(call strip_dotslash, \
+	       $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib))))
+CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES))
+CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
+OBJFILES = $(call vo_to_obj,$(VOFILES))
+ALLNATIVEFILES = \
+	$(OBJFILES:.o=.cmi) \
+	$(OBJFILES:.o=.cmx) \
+	$(OBJFILES:.o=.cmxs)
+# trick: wildcard filters out non-existing files, so that `install` doesn't show
+# warnings and `clean` doesn't pass to rm a list of files that is too long for
+# the shell.
+NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
+FILESTOINSTALL = \
+	$(VOFILES) \
+	$(VFILES) \
+	$(GLOBFILES) \
+	$(NATIVEFILES) \
+	$(CMIFILESTOINSTALL)
+BYTEFILESTOINSTALL = \
+	$(CMOFILESTOINSTALL) \
+	$(CMAFILES)
+ifeq '$(HASNATDYNLINK)' 'true'
+DO_NATDYNLINK = yes
+FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
+else
+DO_NATDYNLINK =
+endif
+
+ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE))
+
+# Compilation targets #########################################################
+
+all:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
+.PHONY: all
+
+all.timing.diff:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES=""
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
+.PHONY: all.timing.diff
+
+make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
+make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
+make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
+	$(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
+print-pretty-timed::
+	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+print-pretty-timed-diff::
+	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ifeq (,$(BEFORE))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
+	$(HIDE)false
+else
+ifeq (,$(AFTER))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
+	$(HIDE)false
+else
+print-pretty-single-time-diff::
+	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+endif
+endif
+pretty-timed:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed
+.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff
+
+# Extension points for actions to be performed before/after the all target
+pre-all::
+	@# Extension point
+	$(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
+	  echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
+	  echo "W: while the current Coq version is $(COQ_VERSION)";\
+	fi
+.PHONY: pre-all
+
+post-all::
+	@# Extension point
+.PHONY: post-all
+
+real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
+.PHONY: real-all
+
+real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff)
+.PHONY: real-all.timing.diff
+
+bytefiles: $(CMOFILES) $(CMAFILES)
+.PHONY: bytefiles
+
+optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
+.PHONY: optfiles
+
+# FIXME, see Ralf's bugreport
+quick: $(VOFILES:.vo=.vio)
+.PHONY: quick
+
+vio2vo:
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: vio2vo
+
+quick2vo:
+	$(HIDE)make -j $(J) quick
+	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
+	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
+	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
+	done); \
+	echo "VIO2VO: $$VIOFILES"; \
+	if [ -n "$$VIOFILES" ]; then \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \
+	fi
+.PHONY: quick2vo
+
+checkproofs:
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: checkproofs
+
+validate: $(VOFILES)
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $^
+.PHONY: validate
+
+only: $(TGTS)
+.PHONY: only
+
+# Documentation targets #######################################################
+
+html: $(GLOBFILES) $(VFILES)
+	$(SHOW)'COQDOC -d html $(GAL)'
+	$(HIDE)mkdir -p html
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
+
+mlihtml: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'CAMLDOC -d $@'
+	$(HIDE)mkdir $@ || rm -rf $@/*
+	$(HIDE)$(CAMLDOC) -html \
+		-d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
+
+all-mli.tex: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'CAMLDOC -latex $@'
+	$(HIDE)$(CAMLDOC) -latex \
+		-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
+
+gallina: $(GFILES)
+
+all.ps: $(VFILES)
+	$(SHOW)'COQDOC -ps $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all.pdf: $(VFILES)
+	$(SHOW)'COQDOC -pdf $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+# FIXME: not quite right, since the output name is different
+gallinahtml: GAL=-g
+gallinahtml: html
+
+all-gal.ps: GAL=-g
+all-gal.ps: all.ps
+
+all-gal.pdf: GAL=-g
+all-gal.pdf: all.pdf
+
+# ?
+beautify: $(BEAUTYFILES)
+	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+	@echo 'Do not do "make clean" until you are sure that everything went well!'
+	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+.PHONY: beautify
+
+# Installation targets ########################################################
+#
+# There rules can be extended in @LOCAL_FILE@
+# Extensions can't assume when they run.
+
+install:
+	$(HIDE)for f in $(FILESTOINSTALL); do\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+	$(HIDE)$(MAKE) install-extra -f "$(SELF)"
+install-extra::
+	@# Extension point
+.PHONY: install install-extra
+
+install-byte:
+	$(HIDE)for f in $(BYTEFILESTOINSTALL); do\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+
+install-doc:: html mlihtml
+	@# Extension point
+	$(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(HIDE)for i in html/*; do \
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
+	done
+	$(HIDE)install -d \
+		"$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE)for i in mlihtml/*; do \
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
+	done
+.PHONY: install-doc
+
+uninstall::
+	@# Extension point
+	$(HIDE)for f in $(FILESTOINSTALL); do \
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
+	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
+	 rm -f "$$instf" &&\
+	 echo RM "$$instf" &&\
+	 (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+	done
+.PHONY: uninstall
+
+uninstall-doc::
+	@# Extension point
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
+.PHONY: uninstall-doc
+
+# Cleaning ####################################################################
+#
+# There rules can be extended in @LOCAL_FILE@
+# Extensions can't assume when they run.
+
+clean::
+	@# Extension point
+	$(SHOW)'CLEAN'
+	$(HIDE)rm -f $(CMOFILES)
+	$(HIDE)rm -f $(CMIFILES)
+	$(HIDE)rm -f $(CMAFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
+	$(HIDE)rm -f $(CMXAFILES)
+	$(HIDE)rm -f $(CMXSFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
+	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
+	$(HIDE)rm -f $(ALLDFILES)
+	$(HIDE)rm -f $(NATIVEFILES)
+	$(HIDE)find . -name .coq-native -type d -empty -delete
+	$(HIDE)rm -f $(VOFILES)
+	$(HIDE)rm -f $(VOFILES:.vo=.vio)
+	$(HIDE)rm -f $(GFILES)
+	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
+	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
+	$(HIDE)rm -f $(VFILES:.v=.glob)
+	$(HIDE)rm -f $(VFILES:.v=.tex)
+	$(HIDE)rm -f $(VFILES:.v=.g.tex)
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)rm -rf html mlihtml
+.PHONY: clean
+
+cleanall:: clean
+	@# Extension point
+	$(SHOW)'CLEAN *.aux *.timing'
+	$(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+	$(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.before-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.after-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff)
+.PHONY: cleanall
+
+archclean::
+	@# Extension point
+	$(SHOW)'CLEAN *.cmx *.o'
+	$(HIDE)rm -f $(NATIVEFILES)
+	$(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
+.PHONY: archclean
+
+
+# Compilation rules ###########################################################
+
+$(MLIFILES:.mli=.cmi): %.cmi: %.mli
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+
+$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4
+	$(SHOW)'CAMLC -pp -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $<
+
+$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4
+	$(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $<
+
+$(MLFILES:.ml=.cmo): %.cmo: %.ml
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+
+$(MLFILES:.ml=.cmx): %.cmx: %.ml
+	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
+
+
+$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-linkall -shared -o $@ $<
+
+$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -linkall -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
+	$(SHOW)'CAMLC -pack -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
+	$(SHOW)'CAMLOPT -pack -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+# This rule is for _CoqProject with no .mllib nor .mlpack
+$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
+	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -o $@ $<
+
+ifneq (,$(TIMING))
+TIMING_EXTRA = > $<.$(TIMING_EXT)
+else
+TIMING_EXTRA =
+endif
+
+$(VOFILES): %.vo: %.v
+	$(SHOW)COQC $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA)
+
+# FIXME ?merge with .vo / .vio ?
+$(GLOBFILES): %.glob: %.v
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
+
+$(VFILES:.v=.vio): %.vio: %.v
+	$(SHOW)COQC -quick $<
+	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+
+$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
+	$(SHOW)PYTHON TIMING-DIFF $<
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
+
+$(BEAUTYFILES): %.v.beautified: %.v
+	$(SHOW)'BEAUTIFY $<'
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
+
+$(GFILES): %.g: %.v
+	$(SHOW)'GALLINA $<'
+	$(HIDE)$(GALLINA) $<
+
+$(TEXFILES): %.tex: %.v
+	$(SHOW)'COQDOC -latex $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+$(GTEXFILES): %.g.tex: %.v
+	$(SHOW)'COQDOC -latex -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+$(HTMLFILES): %.html: %.v %.glob
+	$(SHOW)'COQDOC -html $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+$(GHTMLFILES): %.g.html: %.v %.glob
+	$(SHOW)'COQDOC -html -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
+
+# Dependency files ############################################################
+
+ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
+ -include $(ALLDFILES)
+else
+ ifeq ($(MAKECMDGOALS),)
+  -include $(ALLDFILES)
+ endif
+endif
+
+.SECONDARY: $(ALLDFILES)
+
+redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV )
+
+$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4
+	$(SHOW)'CAMLDEP -pp $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+# If this makefile is created using a _CoqProject we have coqdep get
+# options from it. This avoids argument length limits for pathological
+# projects. Note that extra options might be on the command line.
+VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
+
+$(VDFILE).d: $(VFILES)
+	$(SHOW)'COQDEP VFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+
+# Misc ########################################################################
+
+byte:
+	$(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)"
+.PHONY: byte
+
+opt:
+	$(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
+.PHONY:	opt
+
+# This is deprecated.  To extend this makefile use
+# extension points and @LOCAL_FILE@
+printenv::
+	$(warning printenv is deprecated)
+	$(warning write extensions in @LOCAL_FILE@ or include @CONF_FILE@)
+	@echo 'LOCAL = $(LOCAL)'
+	@echo 'COQLIB = $(COQLIB)'
+	@echo 'DOCDIR = $(DOCDIR)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'CAMLP5O = $(CAMLP5O)'
+	@echo 'CAMLP5BIN = $(CAMLP5BIN)'
+	@echo 'CAMLP5LIB = $(CAMLP5LIB)'
+	@echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)'
+	@echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
+	@echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)'
+	@echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'PP = $(PP)'
+	@echo 'COQFLAGS = $(COQFLAGS)'
+	@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
+.PHONY:	printenv
+
+# Generate a .merlin file.  If you need to append directives to this
+# file you can extend the merlin-hook target in @LOCAL_FILE@
+.merlin:
+	$(SHOW)'FILL .merlin'
+	$(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
+	$(HIDE)echo 'B $(COQLIB)' >> .merlin
+	$(HIDE)echo 'S $(COQLIB)' >> .merlin
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo 'B $(COQLIB)$(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo 'S $(COQLIB)$(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;)
+	$(HIDE)$(MAKE) merlin-hook -f "$(SELF)"
+.PHONY: merlin
+
+merlin-hook::
+	@# Extension point
+.PHONY: merlin-hook
+
+# prints all variables
+debug:
+	$(foreach v,\
+		$(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\
+	       		$(.VARIABLES))),\
+	       	$(info $(v) = $($(v))))
+.PHONY: debug
+
+.DEFAULT_GOAL := all
diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py
new file mode 100644
index 00000000..8564aeff
--- /dev/null
+++ b/tools/TimeFileMaker.py
@@ -0,0 +1,219 @@
+from __future__ import with_statement
+from __future__ import division
+from __future__ import unicode_literals
+from __future__ import print_function
+import os, sys, re
+from io import open
+
+# This script parses the output of `make TIMED=1` into a dictionary
+# mapping names of compiled files to the number of minutes and seconds
+# that they took to compile.
+
+STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?')
+STRIP_REP = r'\1'
+INFINITY  = '\u221e'
+
+def parse_args(argv, USAGE, HELP_STRING):
+    sort_by = 'auto'
+    if any(arg.startswith('--sort-by=') for arg in argv[1:]):
+        sort_by = [arg for arg in argv[1:] if arg.startswith('--sort-by=')][-1][len('--sort-by='):]
+    args = [arg for arg in argv if not arg.startswith('--sort-by=')]
+    if len(args) < 3 or '--help' in args[1:] or '-h' in args[1:] or sort_by not in ('auto', 'absolute', 'diff'):
+        print(USAGE)
+        if '--help' in args[1:] or '-h' in args[1:]:
+            print(HELP_STRING)
+            if len(args) == 2: sys.exit(0)
+        sys.exit(1)
+    return sort_by, args
+
+
+def reformat_time_string(time):
+    seconds, milliseconds = time.split('.')
+    seconds = int(seconds)
+    minutes, seconds = divmod(seconds, 60)
+    return '%dm%02d.%ss' % (minutes, seconds, milliseconds)
+
+def get_times(file_name):
+    '''
+    Reads the contents of file_name, which should be the output of
+    'make TIMED=1', and parses it to construct a dict mapping file
+    names to compile durations, as strings.  Removes common prefixes
+    using STRIP_REG and STRIP_REP.
+    '''
+    if file_name == '-':
+        lines = sys.stdin.read()
+    else:
+        with open(file_name, 'r', encoding="utf-8") as f:
+            lines = f.read()
+    reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE)
+    times = reg.findall(lines)
+    if all(time in ('0.00', '0.01') for name, time in times):
+        reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE)
+        times = reg.findall(lines)
+    if all(STRIP_REG.search(name.strip()) for name, time in times):
+        times = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), time) for name, time in times)
+    return dict((name, reformat_time_string(time)) for name, time in times)
+
+def get_single_file_times(file_name):
+    '''
+    Reads the contents of file_name, which should be the output of
+    'coqc -time', and parses it to construct a dict mapping lines to
+    to compile durations, as strings.
+    '''
+    if file_name == '-':
+        lines = sys.stdin.read()
+    else:
+        with open(file_name, 'r', encoding="utf-8") as f:
+            lines = f.read()
+    reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE)
+    times = reg.findall(lines)
+    if len(times) == 0: return dict()
+    longest = max(max((len(start), len(stop))) for start, stop, name, time, extra in times)
+    FORMAT = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest)
+    return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(time)) for start, stop, name, time, extra in times)
+
+def fix_sign_for_sorting(num, descending=True):
+    return -num if descending else num
+
+def make_sorting_key(times_dict, descending=True):
+    def get_key(name):
+        minutes, seconds = times_dict[name].replace('s', '').split('m')
+        return (fix_sign_for_sorting(int(minutes), descending=descending),
+                fix_sign_for_sorting(float(seconds), descending=descending),
+                name)
+    return get_key
+
+def get_sorted_file_list_from_times_dict(times_dict, descending=True):
+    '''
+    Takes the output dict of get_times and returns the list of keys,
+    sorted by duration.
+    '''
+    return sorted(times_dict.keys(), key=make_sorting_key(times_dict, descending=descending))
+
+def to_seconds(time):
+    '''
+    Converts a string time into a number of seconds.
+    '''
+    minutes, seconds = time.replace('s', '').split('m')
+    sign = -1 if time[0] == '-' else 1
+    return sign * (abs(int(minutes)) * 60 + float(seconds))
+
+def from_seconds(seconds, signed=False):
+    '''
+    Converts a number of seconds into a string time.
+    '''
+    sign = ('-' if seconds < 0 else '+') if signed else ''
+    seconds = abs(seconds)
+    minutes = int(seconds) // 60
+    seconds -= minutes * 60
+    full_seconds = int(seconds)
+    partial_seconds = int(100 * (seconds - full_seconds))
+    return sign + '%dm%02d.%02ds' % (minutes, full_seconds, partial_seconds)
+
+def sum_times(times, signed=False):
+    '''
+    Takes the values of an output from get_times, parses the time
+    strings, and returns their sum, in the same string format.
+    '''
+    # sort the times before summing because floating point addition is not associative
+    return from_seconds(sum(sorted(map(to_seconds, times))), signed=signed)
+
+def format_percentage(num, signed=True):
+    sign = ('-' if num < 0 else '+') if signed else ''
+    num = abs(num)
+    whole_part = int(num * 100)
+    frac_part = int(100 * (num * 100 - whole_part))
+    return sign + '%d.%02d%%' % (whole_part, frac_part)
+
+def make_diff_table_string(left_times_dict, right_times_dict,
+                           sort_by='auto',
+                           descending=True,
+                           left_tag="After", tag="File Name", right_tag="Before", with_percent=True,
+                           change_tag="Change", percent_change_tag="% Change"):
+    # We first get the names of all of the compiled files: all files
+    # that were compiled either before or after.
+    all_names_dict = dict()
+    all_names_dict.update(right_times_dict)
+    all_names_dict.update(left_times_dict) # do the left (after) last, so that we give precedence to those ones
+    if len(all_names_dict.keys()) == 0: return 'No timing data'
+    prediff_times = tuple((name, to_seconds(left_times_dict.get(name,'0m0.0s')), to_seconds(right_times_dict.get(name,'0m0.0s')))
+                          for name in all_names_dict.keys())
+    diff_times_dict = dict((name, from_seconds(lseconds - rseconds, signed=True))
+                           for name, lseconds, rseconds in prediff_times)
+    percent_diff_times_dict = dict((name, ((format_percentage((lseconds - rseconds) / rseconds))
+                                           if rseconds != 0 else (INFINITY if lseconds > 0 else 'N/A')))
+                                   for name, lseconds, rseconds in prediff_times)
+    # update to sort by approximate difference, first
+    get_key_abs = make_sorting_key(all_names_dict, descending=descending)
+    get_key_diff_float = (lambda name: fix_sign_for_sorting(to_seconds(diff_times_dict[name]), descending=descending))
+    get_key_diff_absint = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending))
+    if sort_by == 'absolute':
+        get_key = get_key_abs
+    elif sort_by == 'diff':
+        get_key = get_key_diff_float
+    else: # sort_by == 'auto'
+        get_key = (lambda name: (get_key_diff_absint(name), get_key_abs(name)))
+    names = sorted(all_names_dict.keys(), key=get_key)
+    #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending)
+    # set the widths of each of the columns by the longest thing to go in that column
+    left_sum = sum_times(left_times_dict.values())
+    right_sum = sum_times(right_times_dict.values())
+    left_sum_float = sum(sorted(map(to_seconds, left_times_dict.values())))
+    right_sum_float = sum(sorted(map(to_seconds, right_times_dict.values())))
+    diff_sum = from_seconds(left_sum_float - right_sum_float, signed=True)
+    percent_diff_sum = (format_percentage((left_sum_float - right_sum_float) / right_sum_float)
+                        if right_sum_float > 0 else 'N/A')
+    left_width = max(max(map(len, ['N/A'] + list(left_times_dict.values()))), len(left_sum))
+    right_width = max(max(map(len, ['N/A'] + list(right_times_dict.values()))), len(right_sum))
+    far_right_width = max(max(map(len, ['N/A', change_tag] + list(diff_times_dict.values()))), len(diff_sum))
+    far_far_right_width = max(max(map(len, ['N/A', percent_change_tag] + list(percent_diff_times_dict.values()))), len(percent_diff_sum))
+    middle_width = max(map(len, names + [tag, "Total"]))
+    format_string = ("%%(left)-%ds | %%(middle)-%ds | %%(right)-%ds || %%(far_right)-%ds"
+                     % (left_width, middle_width, right_width, far_right_width))
+    if with_percent:
+        format_string += " | %%(far_far_right)-%ds" % far_far_right_width
+    header = format_string % {'left': left_tag, 'middle': tag, 'right': right_tag, 'far_right': change_tag, 'far_far_right': percent_change_tag}
+    total = format_string % {'left': left_sum, 'middle': "Total", 'right': right_sum, 'far_right': diff_sum, 'far_far_right': percent_diff_sum}
+    # separator to go between headers and body
+    sep = '-' * len(header)
+    # the representation of the default value (0), to get replaced by N/A
+    left_rep, right_rep, far_right_rep, far_far_right_rep = ("%%-%ds | " % left_width) % 0, (" | %%-%ds || " % right_width) % 0, ("|| %%-%ds" % far_right_width) % 0, ("| %%-%ds" % far_far_right_width) % 0
+    return '\n'.join([header, sep, total, sep] +
+                     [format_string % {'left': left_times_dict.get(name, 0),
+                                       'middle': name,
+                                       'right': right_times_dict.get(name, 0),
+                                       'far_right': diff_times_dict.get(name, 0),
+                                       'far_far_right': percent_diff_times_dict.get(name, 0)}
+                      for name in names]).replace(left_rep, 'N/A'.center(len(left_rep) - 3) + ' | ').replace(right_rep, ' | ' + 'N/A'.center(len(right_rep) - 7) + ' || ').replace(far_right_rep, '|| ' + 'N/A'.center(len(far_right_rep) - 3)).replace(far_far_right_rep, '| ' + 'N/A'.center(len(far_far_right_rep) - 2))
+
+def make_table_string(times_dict,
+                      descending=True,
+                      tag="Time"):
+    if len(times_dict.keys()) == 0: return 'No timing data'
+    # We first get the names of all of the compiled files, sorted by
+    # duration
+    names = get_sorted_file_list_from_times_dict(times_dict, descending=descending)
+    # compute the widths of the columns
+    times_width = max(max(map(len, times_dict.values())), len(sum_times(times_dict.values())))
+    names_width = max(map(len, names + ["File Name", "Total"]))
+    format_string = "%%-%ds | %%-%ds" % (times_width, names_width)
+    header = format_string % (tag, "File Name")
+    total = format_string % (sum_times(times_dict.values()),
+                             "Total")
+    sep = '-' * len(header)
+    return '\n'.join([header, sep, total, sep] +
+                     [format_string % (times_dict[name],
+                                       name)
+                      for name in names])
+
+def print_or_write_table(table, files):
+    if len(files) == 0 or '-' in files:
+        try:
+            binary_stdout = sys.stdout.buffer
+        except AttributeError:
+            binary_stdout = sys.stdout
+        print(table.encode("utf-8"), file=binary_stdout)
+    for file_name in files:
+        if file_name != '-':
+            with open(file_name, 'w', encoding="utf-8") as f:
+                f.write(table)
diff --git a/tools/beautify-archive b/tools/beautify-archive
index 6bfa974a..a327ea44 100755
--- a/tools/beautify-archive
+++ b/tools/beautify-archive
@@ -23,7 +23,7 @@ cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE
 cd $NEWARCHIVE
 rm description || true
 make clean
-make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
+make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS)' || \
  { echo ---- Failed to beautify; exit 1; }
 echo -------- Upgrading files in the beautification directory --------------
 beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX`
diff --git a/tools/check-translate b/tools/check-translate
index 3dd82405..acb6f459 100755
--- a/tools/check-translate
+++ b/tools/check-translate
@@ -2,7 +2,7 @@
 
 echo -------------- Producing translated files ---------------------
 rm */*/*.v8 >& /dev/null
-make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; }
+make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; }
 if [ -e translated ]; then rm -r translated; fi
 if [ -e successful-translation ]; then rm -r successful-translation; fi
 if [ -e failed-translation ]; then rm -r failed-translation; fi
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index eab909f5..5402765f 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -1,24 +1,24 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Coq_makefile: automatically create a Makefile for a Coq development *)
 
+open CoqProject_file
+open Printf
+
+let (>) f g = fun x -> g (f x)
+
 let output_channel = ref stdout
 let makefile_name = ref "Makefile"
 let make_name = ref ""
 
-let some_vfile = ref false
-let some_mlfile = ref false
-let some_mlifile = ref false
-let some_ml4file = ref false
-let some_mllibfile = ref false
-let some_mlpackfile = ref false
-
 let print x = output_string !output_channel x
 let printf x = Printf.fprintf !output_channel x
 
@@ -31,85 +31,58 @@ let rec print_prefix_list sep = function
   | x :: l -> print sep; print x; print_prefix_list sep l
   | [] -> ()
 
-let section s =
-  let l = String.length s in
-  let print_com s =
-    print "#";
-    print s;
-    print "#\n" in
-  print_com (String.make (l+2) '#');
-  print_com (String.make (l+2) ' ');
-  print "# "; print s; print " #\n";
-  print_com (String.make (l+2) ' ');
-  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"; "ltacprof";
-   "toplevel"; "stm"; "grammar"; "config";
-   "ltac"; "engine"]
-
-
-let usage () =
-  output_string stderr "Usage summary:
-
-coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]
-  ... [any] ... [-extra[-phony] result dependencies command]
-  ... [-I dir] ... [-R physicalpath logicalpath]
-  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]
-  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
-  [-h] [--help]
-
-[file.v]: Coq file to be compiled
-[file.ml[i4]?]: Objective Caml file to be compiled
-[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml
-  library/module
-[any] : subdirectory that should be \"made\" and has a Makefile itself
-  to do so. Very fragile and discouraged.
-[-extra result dependencies command]: add target \"result\" with command
-  \"command\" and dependencies \"dependencies\". If \"result\" is not
-  generic (do not contains a %), \"result\" is built by _make all_ and
-  deleted by _make clean_.
-[-extra-phony result dependencies command]: add a PHONY target \"result\"
- with command \"command\" and dependencies \"dependencies\". Note that
- _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as
- as a dependencies of an already defined target \"foo\".
-[-I dir]: look for Objective Caml dependencies in \"dir\"
-[-R physicalpath logicalpath]: look for Coq dependencies resursively
-  starting from \"physicalpath\". The logical path associated to the
-  physical path is \"logicalpath\".
-[-Q physicalpath logicalpath]: look for Coq dependencies starting from
-  \"physicalpath\". The logical path associated to the physical path
-  is \"logicalpath\".
-[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
-[-byte]: compile with byte-code version of coq
-[-opt]: compile with native-code version of coq
-[-arg opt]: send option \"opt\" to coqc
-[-install opt]: where opt is \"user\" to force install into user directory,
-  \"none\" to build a makefile with no install target or
-  \"global\" to force install in $COQLIB directory
-[-f file]: take the contents of file as arguments
-[-o file]: output should go in file file
-	Output file outside the current directory is forbidden.
-[-h]: print this usage summary
-[--help]: equivalent to [-h]\n";
+let usage_coq_makefile () =
+  output_string stderr "Usage summary:\
+\n\
+\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
+\n  ... [any] ... [-extra[-phony] result dependencies command]\
+\n  ... [-I dir] ... [-R physicalpath logicalpath]\
+\n  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
+\n  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
+\n  [-h] [--help]\
+\n";
+  output_string stderr "\
+\nFull list of options:\
+\n\
+\n[file.v]: Coq file to be compiled\
+\n[file.ml[i4]?]: Objective Caml file to be compiled\
+\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
+\n  library/module\
+\n[any] : subdirectory that should be \"made\" and has a Makefile itself\
+\n  to do so. Very fragile and discouraged.\
+\n[-extra result dependencies command]: add target \"result\" with command\
+\n  \"command\" and dependencies \"dependencies\". If \"result\" is not\
+\n  generic (do not contains a %), \"result\" is built by _make all_ and\
+\n  deleted by _make clean_.\
+\n[-extra-phony result dependencies command]: add a PHONY target \"result\"\
+\n with command \"command\" and dependencies \"dependencies\". Note that\
+\n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\
+\n as a dependencies of an already defined target \"foo\".\
+\n[-I dir]: look for Objective Caml dependencies in \"dir\"\
+\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\
+\n  starting from \"physicalpath\". The logical path associated to the\
+\n  physical path is \"logicalpath\".\
+\n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\
+\n  \"physicalpath\". The logical path associated to the physical path\
+\n  is \"logicalpath\".\
+\n[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"\
+\n[-byte]: compile with byte-code version of coq\
+\n[-opt]: compile with native-code version of coq\
+\n[-arg opt]: send option \"opt\" to coqc\
+\n[-install opt]: where opt is \"user\" to force install into user directory,\
+\n  \"none\" to build a makefile with no install target or\
+\n  \"global\" to force install in $COQLIB directory\
+\n[-f file]: take the contents of file as arguments\
+\n[-o file]: output should go in file file (recommended)\
+\n	Output file outside the current directory is forbidden.\
+\n[-h]: print this usage summary\
+\n[--help]: equivalent to [-h]\n";
   exit 1
 
 let is_genrule r = (* generic rule (like bar%foo: ...) *)
     let genrule = Str.regexp("%") in
       Str.string_match genrule r 0
 
-let string_prefix a b =
-  let rec aux i =
-    try if a.[i] = b.[i] then aux (i+1) else i with Invalid_argument _ -> i
-  in
-  String.sub a 0 (aux 0)
-
 let is_prefix dir1 dir2 =
   let l1 = String.length dir1 in
   let l2 = String.length dir2 in
@@ -122,836 +95,348 @@ let is_prefix dir1 dir2 =
   else false
 
 let physical_dir_of_logical_dir ldir =
-  let le = String.length ldir - 1 in
+  let ldir = Bytes.of_string ldir in
+  let le = Bytes.length ldir - 1 in
   let pdir =
-    if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1)
-    else String.copy ldir
+    if le >= 0 && Bytes.get ldir le = '.' then Bytes.sub ldir 0 (le - 1)
+    else Bytes.copy ldir
   in
   for i = 0 to le - 1 do
-    if pdir.[i] = '.' then pdir.[i] <- '/';
+    if Bytes.get pdir i = '.' then Bytes.set pdir i '/';
   done;
-  pdir
-
-let standard opt =
-  print "byte:\n";
-  print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
-  print "opt:\n";
-  if not opt then print "\t@echo \"WARNING: opt is disabled\"\n";
-  print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte");
-  print "\"\n\n"
-
-let classify_files_by_root var files (inc_ml,inc_i,inc_r) =
-  if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r ||
-     List.exists (fun (pdir,_,_) -> pdir = ".") inc_i
-  then ()
-  else
-    let absdir_of_files =List.rev_map
-	(fun x -> CUnix.canonical_path_name (Filename.dirname x))
-	files
-    in
-    (* files in scope of a -I option (assuming they are no overlapping) *)
-    if List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml then
-      begin
-	printf "%sINC=" var;
-	List.iter (fun (pdir,absdir) ->
-		   if List.mem absdir absdir_of_files
-		   then printf "$(filter $(wildcard %s/*),$(%s)) " pdir var)
-		  inc_ml;
-	printf "\n";
-      end;
-    (* Files in the scope of a -R option (assuming they are disjoint) *)
-    List.iteri (fun i (pdir,_,abspdir) ->
-		if List.exists (is_prefix abspdir) absdir_of_files then
-		  printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n"
-			 var i pdir pdir var)
-	       (inc_i@inc_r)
-
-let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
-  let var_x_absdirs_l =
-    List.rev_map
-      (fun (v,l) ->
-       (v,List.rev_map
-            (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l))
-      var_x_files_l
-  in
-  let var_filter f g =
-    List.fold_left
-      (fun acc (var,dirs) -> if f dirs then (g var)::acc else acc)
-      [] var_x_absdirs_l
-  in
-  (* All files caught by a -R . option (assuming it is the only one) *)
-  match inc_i@inc_r with
-  |[(".",t,_)] ->
-    (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l])
-  |l ->
-    try
-      let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
-      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n"
-      in
-      (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
-    with Not_found ->
-      (* vars for -Q options *)
-      let varq = var_filter
-                   (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml)
-                   (fun x -> x)
-      in
-      (* (physical dir, physical dir of logical path,vars) for -R options
-	 (assuming physical dirs are disjoint) *)
-      let other =
-        if l = [] then
-	  [".","$(INSTALLDEFAULTROOT)",[]]
-        else
-	  Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) ->
-	    let vars_r = var_filter
-                           (List.exists (is_prefix abspdir))
-                           (fun x -> x^string_of_int i)
-            in
-	    let pdir' = physical_dir_of_logical_dir ldir in
-	    (pdir,pdir',vars_r)::out) 0 [] l
-      in (Some varq, other)
-
-let install_include_by_root perms =
-  let install_dir for_i (pdir,pdir',vars) =
-    let b = vars <> [] in
-    if b then begin
-      printf "\tcd \"%s\" && for i in " pdir;
-      print_list " " (List.rev_map (Format.sprintf "$(%s)") vars);
-      print "; do \\\n";
-      printf "\t install -d \"`dirname \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i`\"; \\\n" pdir';
-      printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i; \\\n" perms pdir';
-      printf "\tdone\n";
-    end;
-    for_i b pdir' in
-  let install_i = function
-    |[] -> fun _ _ -> ()
-    |l -> fun b d ->
-      if not b then printf "\tinstall -d \"$(DSTROOT)\"$(COQLIBINSTALL)/%s; \\\n" d;
-      print "\tfor i in ";
-      print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l);
-      print "; do \\\n";
-      printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" perms d;
-      printf "\tdone\n"
-  in function
-  |None,l -> List.iter (install_dir (fun _ _ -> ())) l
-  |Some v_i,l -> List.iter (install_dir (install_i v_i)) l
-
-let uninstall_by_root =
-  let uninstall_dir for_i (pdir,pdir',vars) =
-    printf "\tprintf 'cd \"$${DSTROOT}\"$(COQLIBINSTALL)/%s" pdir';
-    if vars <> [] then begin
-      print " && rm -f ";
-      print_list " " (List.rev_map (Format.sprintf "$(%s)") vars);
-    end;
-    for_i ();
-    print " && find . -type d -and -empty -delete\\n";
-    print "cd \"$${DSTROOT}\"$(COQLIBINSTALL) && ";
-    printf "find \"%s\" -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" pdir'
-in
-  let uninstall_i = function
-    |[] -> ()
-    |l ->
-      print " && \\\\\\nfor i in ";
-      print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l);
-      print "; do rm -f \"`basename \"$$i\"`\"; done"
-  in function
-  |None,l -> List.iter (uninstall_dir (fun _ -> ())) l
-  |Some v_i,l -> List.iter (uninstall_dir (fun () -> uninstall_i v_i)) l
-
-let where_put_doc = function
-    |_,[],[] -> "$(INSTALLDEFAULTROOT)";
-    |_,((_,lp,_)::q as inc_i),[] ->
-      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
-      if (pr <> "") &&
-	((List.exists (fun(_,b,_) -> b = pr) inc_i)
-	 || pr.[String.length pr - 1] = '.')
-      then
-	physical_dir_of_logical_dir pr
-      else
-	let () = prerr_string "Warning: -Q options don't have a correct common prefix,
- install-doc will put anything in $INSTALLDEFAULTROOT\n" in
-	"$(INSTALLDEFAULTROOT)"
-    |_,inc_i,((_,lp,_)::q as inc_r) ->
-      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
-      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) pr inc_i in
-      if (pr <> "") &&
-	((List.exists (fun(_,b,_) -> b = pr) inc_r)
-	 || (List.exists (fun(_,b,_) -> b = pr) inc_i)
-	 || pr.[String.length pr - 1] = '.')
-      then
-	physical_dir_of_logical_dir pr
-      else
-	let () = prerr_string "Warning: -R/-Q options don't have a correct common prefix,
- install-doc will put anything in $INSTALLDEFAULTROOT\n" in
-	"$(INSTALLDEFAULTROOT)"
-
-let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
-  |Project_file.NoInstall -> ()
-  |is_install ->
-    let not_empty = function |[] -> false |_::_ -> true in
-    let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in
-    let cmis = List.rev_append mlis cmos in
-    let cmxss = List.rev_append cmos mllibs in
-    let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in
-    let where_what_oth = vars_to_put_by_root
-      [("VOFILES",vfiles);("VFILES",vfiles);
-       ("GLOBFILES",vfiles);("NATIVEFILES",vfiles);
-       ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)]
-      inc in
-    let doc_dir = where_put_doc inc in
-    if is_install = Project_file.UnspecInstall then begin
-	print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n"
-    end;
-    if not_empty cmxss then begin
-      print "install-natdynlink:\n";
-      install_include_by_root "0755" where_what_cmxs;
-      print "\n";
-    end;
-    if not_empty cmxss then begin
-      print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
-      printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
-      printf "\t install -m 0755 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
-      print "\n";
-    end;
-    print "install:";
-    if not_empty cmxss then begin
-      print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)";
+  Bytes.to_string pdir
+
+let read_whole_file s =
+  let ic = open_in s in
+  let b = Buffer.create (1 lsl 12) in
+  try
+     while true do
+       let s = input_line ic in
+       Buffer.add_string b s;
+       Buffer.add_char b '\n';
+     done;
+     assert false;
+  with End_of_file ->
+    close_in ic;
+    Buffer.contents b
+
+let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s
+
+let generate_makefile oc conf_file local_file args project =
+  let makefile_template =
+    let template = "/tools/CoqMakefile.in" in
+    Envars.coqlib () ^ template in
+  let s = read_whole_file makefile_template in
+  let s = List.fold_left
+    (* We use global_substitute to avoid running into backslash issues due to \1 etc. *)
+    (fun s (k,v) -> Str.global_substitute (Str.regexp_string k) (fun _ -> v) s) s
+    [ "@CONF_FILE@", conf_file;
+      "@LOCAL_FILE@", local_file;
+      "@COQ_VERSION@", Coq_config.version;
+      "@PROJECT_FILE@", (Option.default "" project.project_file);
+      "@COQ_MAKEFILE_INVOCATION@",String.concat " " (List.map quote args);
+    ] in
+  output_string oc s
+;;
+
+let section oc s =
+  let pad = String.make (76 - String.length s) ' ' in
+  let sharps = String.make 79 '#' in
+  let spaces = "#" ^ String.make 77 ' ' ^ "#" in
+  fprintf oc "\n%s\n" sharps;
+  fprintf oc "%s\n" spaces;
+  fprintf oc "# %s%s#\n" s pad;
+  fprintf oc "%s\n" spaces;
+  fprintf oc "%s\n\n" sharps
+;;
+
+let clean_tgts = ["clean"; "cleanall"; "archclean"]
+
+let generate_conf_extra_target oc sps =
+  let pr_path { target; dependencies; phony; command } =
+    let target = if target = "all" then "custom-all" else target in
+    if phony then fprintf oc ".PHONY: %s\n" target;
+    if not (is_genrule target) && not phony then begin
+      fprintf oc "post-all::\n\t$(MAKE) -f $(SELF) %s\n" target;
+      if not phony then
+        fprintf oc "clean::\n\trm -f %s\n" target;
     end;
-    print "\n";
-    install_include_by_root "0644" where_what_oth;
-    List.iter
-      (fun x ->
-	printf "\t+cd %s && $(MAKE) DSTROOT=\"$(DSTROOT)\" INSTALLDEFAULTROOT=\"$(INSTALLDEFAULTROOT)/%s\" install\n" x x)
-      sds;
-    print "\n";
-    let install_one_kind kind dir =
-      printf "\tinstall -d \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/%s\n" dir kind;
-      printf "\tfor i in %s/*; do \\\n" kind;
-      printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/$$i;\\\n" dir;
-      print "\tdone\n" in
-    print "install-doc:\n";
-    if not_empty vfiles then install_one_kind "html" doc_dir;
-    if not_empty mlis then install_one_kind "mlihtml" doc_dir;
-    print "\n";
-    let uninstall_one_kind kind dir =
-      printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir;
-      printf "\tprintf '&& rm -f $(shell find \"%s\" -maxdepth 1 -and -type f -print)\\n' >> \"$@\"\n" kind;
-      print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && ";
-      printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind
-    in
-    printf "uninstall_me.sh: %s\n" !makefile_name;
-    print "\techo '#!/bin/sh' > $@\n";
-    if not_empty cmxss then uninstall_by_root where_what_cmxs;
-    uninstall_by_root where_what_oth;
-    if not_empty vfiles then uninstall_one_kind "html" doc_dir;
-    if not_empty mlis then uninstall_one_kind "mlihtml" doc_dir;
-    print "\tchmod +x $@\n";
-    print "\n";
-    print "uninstall: uninstall_me.sh\n";
-    print "\tsh $<\n\n"
-
-let make_makefile sds =
-  if !make_name <> "" then begin
-    printf "%s: %s\n" !makefile_name !make_name;
-    print "\tmv -f $@ $@.bak\n";
-    print "\t\"$(COQBIN)coq_makefile\" -f $< -o $@\n\n";
-    List.iter
-      (fun x -> print "\t+cd "; print x; print " && $(MAKE) Makefile\n")
-      sds;
-    print "\n";
+    fprintf oc "%s %s %s\n\t%s\n\n"
+       target
+       (if List.mem target clean_tgts then ":: " else ": ")
+       dependencies
+       command
+  in
+    if sps <> [] then
+      section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)";
+    List.iter (forget_source > pr_path) sps
+
+let generate_conf_subdirs oc sds =
+  if sds <> [] then section oc "Subdirectories. (DEPRECATED)";
+  let iter f = List.iter (forget_source > f) in
+  iter (fprintf oc ".PHONY:%s\n") sds;
+  iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
+  iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
+  iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
+  iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
+   
+
+let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
+  section oc "Path directives (-I, -R, -Q).";
+  let module S = String in
+  let map = map_sourced_list in
+  let dash1 opt v = sprintf "-%s %s" opt (quote v) in
+  let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in
+  fprintf oc "COQMF_OCAMLLIBS = %s\n"
+    (S.concat " " (map (fun { path } -> dash1 "I" path) ml_includes));
+  fprintf oc "COQMF_SRC_SUBDIRS = %s\n"
+    (S.concat " " (map (fun { path } -> quote path) ml_includes));
+  fprintf oc "COQMF_COQLIBS = %s %s %s\n"
+    (S.concat " " (map (fun { path } -> dash1 "I" path) ml_includes))
+    (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes))
+    (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes));
+  fprintf oc "COQMF_COQLIBS_NOML = %s %s\n"
+    (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes))
+    (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes));
+  fprintf oc "COQMF_CMDLINE_COQLIBS = %s %s %s\n"
+    (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes))
+    (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes))
+    (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "R" path l) r_includes));
+;;
+
+let windrive s =
+  if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0)
+  then Str.matched_string s
+  else ""
+;;
+
+let generate_conf_coq_config oc args =
+  section oc "Coq configuration.";
+  let src_dirs = Coq_config.all_src_dirs in
+  Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
+  fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib)
+;;
+
+let generate_conf_files oc
+  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; }
+=
+  let module S = String in
+  let map = map_sourced_list in
+  section oc "Project files.";
+  fprintf oc "COQMF_VFILES = %s\n"      (S.concat " " (map quote v_files));
+  fprintf oc "COQMF_MLIFILES = %s\n"    (S.concat " " (map quote mli_files));
+  fprintf oc "COQMF_MLFILES = %s\n"     (S.concat " " (map quote ml_files));
+  fprintf oc "COQMF_ML4FILES = %s\n"    (S.concat " " (map quote ml4_files));
+  fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files));
+  fprintf oc "COQMF_MLLIBFILES = %s\n"  (S.concat " " (map quote mllib_files));
+  let cmdline_vfiles = filter_cmdline v_files in
+  fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (List.map quote cmdline_vfiles));
+;;
+
+let rec all_start_with prefix = function
+  | [] -> true
+  | [] :: _ -> false
+  | (x :: _) :: rest -> x = prefix && all_start_with prefix rest
+
+let rec logic_gcd acc = function
+  | [] -> acc
+  | [] :: _ -> acc
+  | (hd :: tl) :: rest ->
+      if all_start_with hd rest
+      then logic_gcd (acc @ [hd]) (tl :: List.map List.tl rest)
+      else acc
+
+let generate_conf_doc oc { defs; q_includes; r_includes } =
+  let includes = List.map (forget_source > snd) (q_includes @ r_includes) in
+  let logpaths = List.map (CString.split '.') includes in
+  let gcd = logic_gcd [] logpaths in
+  let root =
+    if gcd = [] then
+      if not (List.exists (fun x -> fst x.thing = "INSTALLDEFAULTROOT") defs) then begin
+         let destination = "orphan_" ^ (String.concat "_" includes) in
+         eprintf "Warning: no common logical root\n";
+         eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n";
+         eprintf "Warning: the install-doc target is going to install files\n";
+         eprintf "Warning: in %s\n" destination;
+         destination
+      end else "$(INSTALLDEFAULTROOT)"
+    else String.concat "/" gcd in
+  Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root)
+
+let generate_conf_defs oc { defs; extra_args } =
+  section oc "Extra variables.";
+  List.iter (forget_source > (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v)) defs;
+  Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n"
+    (String.concat " " (List.map forget_source extra_args))
+
+let generate_conf oc project args  =
+  fprintf oc "# This configuration file was generated by running:\n";
+  fprintf oc "# %s\n\n" (String.concat " " (List.map quote args));
+  generate_conf_files oc project;
+  generate_conf_includes oc project;
+  generate_conf_coq_config oc args;
+  generate_conf_defs oc project;
+  generate_conf_doc oc project;
+  generate_conf_extra_target oc project.extra_targets;
+  generate_conf_subdirs oc project.subdirs;
+;;
+
+let ensure_root_dir
+  ({ ml_includes; r_includes; q_includes;
+     v_files; ml_files; mli_files; ml4_files;
+     mllib_files; mlpack_files } as project)
+  =
+  let exists f = List.exists (forget_source > f) in
+  let here = Sys.getcwd () in
+  let not_tops = List.for_all (fun s -> s.thing <> Filename.basename s.thing) in
+  if exists (fun { canonical_path = x } -> x = here) ml_includes
+  || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
+  || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes
+  || (not_tops v_files &&
+      not_tops mli_files && not_tops ml4_files && not_tops ml_files &&
+      not_tops mllib_files && not_tops mlpack_files)
+  then
+    project
+  else
+    let source x = {thing=x; source=CmdLine} in
+    let here_path = { path = "."; canonical_path = here } in
+    { project with
+        ml_includes = source here_path :: ml_includes;
+        r_includes = source (here_path, "Top") :: r_includes }
+;;
+
+let warn_install_at_root_directory 
+  ({ q_includes; r_includes; } as project)
+=
+  let open CList in
+  let inc_top_p =
+    map_filter
+      (fun {thing=({ path } ,ldir)} -> if ldir = "" then Some path else None)
+      (r_includes @ q_includes) in
+  let files = all_files project in
+  let bad = filter (fun f -> mem (Filename.dirname f.thing) inc_top_p) files in
+  if bad <> [] then begin
+    eprintf "Warning: No file should be installed at the root of Coq's library.\n";
+    eprintf "Warning: No logical path (-R, -Q) applies to these files:\n";
+    List.iter (fun x -> eprintf "Warning:  %s\n" x.thing) bad;
+    eprintf "\n";
   end
+;;
 
-let clean sds sps =
-  print "clean::\n";
-  if !some_mlfile || !some_mlifile || !some_ml4file
-     || !some_mllibfile || !some_mlpackfile
-  then
-    begin
-      print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n";
-      print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n";
-      print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n";
-    end;
-  if !some_vfile then
-    begin
-      print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n";
-      print "\tfind . -name .coq-native -type d -empty -delete\n";
-      print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"
-    end;
-  print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n";
-  print "\t- rm -rf html mlihtml uninstall_me.sh\n";
-  List.iter
-    (fun (file,_,is_phony,_) ->
-       if not (is_phony || is_genrule file) then
-	 (print "\t- rm -rf "; print file; print "\n"))
-    sps;
-  List.iter
-    (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n")
-    sds;
-  print "\n";
-  let () =
-    if !some_vfile then
-      let () = print "cleanall:: clean\n" in
-      print "\trm -f $(patsubst %.v,.%.aux,$(VFILES))\n\n" in
-  print "archclean::\n";
-  print "\trm -f *.cmx *.o\n";
-  List.iter
-    (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n")
-    sds;
-  print "\n";
-  print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n";
-  print "\t@echo 'OCAMLFIND =\t$(OCAMLFIND)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
-  print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n"
-
-let header_includes () = ()
-
-let implicit () =
-    section "Implicit rules.";
-  let mli_rules () =
-    print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n";
-    print "\t$(SHOW)'CAMLC -c $<'\n";
-    print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n";
-    print "\t$(SHOW)'CAMLDEP $<'\n";
-    print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
-  in
-  let ml4_rules () =
-    print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n";
-    print "\t$(SHOW)'CAMLC -pp -c $<'\n";
-    print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
-    print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n";
-    print "\t$(SHOW)'CAMLOPT -pp -c $<'\n";
-    print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
-    print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n";
-    print "\t$(SHOW)'CAMLDEP -pp $<'\n";
-    print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
-  let ml_rules () =
-    print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n";
-    print "\t$(SHOW)'CAMLC -c $<'\n";
-    print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n";
-    print "\t$(SHOW)'CAMLOPT -c $<'\n";
-    print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n";
-    print "\t$(SHOW)'CAMLDEP $<'\n";
-    print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
-  let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *)
-    print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx\n";
-    print "\t$(SHOW)'CAMLOPT -shared -o $@'\n";
-    print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n";
-    print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n";
-    print "\t$(SHOW)'CAMLOPT -shared -o $@'\n";
-    print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"
-  in
-  let mllib_rules () =
-    print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n";
-    print "\t$(SHOW)'CAMLC -a -o $@'\n";
-    print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
-    print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n";
-    print "\t$(SHOW)'CAMLOPT -a -o $@'\n";
-    print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
-    print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n";
-    print "\t$(SHOW)'COQDEP $<'\n";
-    print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
-  in
-  let mlpack_rules () =
-    print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n";
-    print "\t$(SHOW)'CAMLC -pack -o $@'\n";
-    print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
-    print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n";
-    print "\t$(SHOW)'CAMLOPT -pack -o $@'\n";
-    print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
-    print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n";
-    print "\t$(SHOW)'COQDEP $<'\n";
-    print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
+let check_overlapping_include { q_includes; r_includes } =
+  let pwd = Sys.getcwd () in
+  let aux = function
+    | [] -> ()
+    | {thing = { path; canonical_path }, _} :: l ->
+	if not (is_prefix pwd canonical_path) then
+	  eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path;
+        List.iter (fun {thing={ path = p; canonical_path = cp }, _} ->
+	  if is_prefix canonical_path cp  || is_prefix cp canonical_path then
+	    eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n"
+              path p) l
   in
-  let v_rules () =
-    print "$(VOFILES): %.vo: %.v\n";
-    print "\t$(SHOW)COQC $<\n";
-    print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
-    print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
-    print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n";
-    print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n";
-    print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
-    print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
-    print "$(VFILES:.v=.g.tex): %.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
-    print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@\n\n";
-    print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n";
-    print "\t$(SHOW)'COQDEP $<'\n";
-    print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
-    print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n"
+    aux (q_includes @ r_includes)
+;;
+
+let chop_prefix p f =
+  let len_p = String.length p in
+  let len_f = String.length f in
+  String.sub f len_p (len_f - len_p)
+
+let clean_path p =
+  Str.global_replace (Str.regexp_string "//") "/" p
+
+let destination_of { ml_includes; q_includes; r_includes; } file =
+  let file_dir = CUnix.canonical_path_name (Filename.dirname file) in
+  let includes = q_includes @ r_includes in
+  let mk_destination logic canonical_path =
+    clean_path (physical_dir_of_logical_dir logic ^ "/" ^
+                chop_prefix canonical_path file_dir ^ "/") in
+  let candidates =
+    CList.map_filter (fun {thing={ canonical_path }, logic} ->
+      if is_prefix canonical_path file_dir then
+        Some(mk_destination logic canonical_path)
+      else None) includes
   in
-    if !some_mlifile then mli_rules ();
-    if !some_ml4file then ml4_rules ();
-    if !some_mlfile then ml_rules ();
-    if !some_mlfile || !some_ml4file then cmxs_rules ();
-    if !some_mllibfile then mllib_rules ();
-    if !some_mlpackfile then mlpack_rules ();
-    if !some_vfile then v_rules ()
-
-let variables is_install opt (args,defs) =
-  let var_aux (v,def) = print v; print "="; print def; print "\n" in
-    section "Variables definitions.";
-    List.iter var_aux defs;
-    print "\n";
-    if not opt then
-      print "override OPT:=-byte\n"
-    else
-      print "OPT?=\n";
-    begin
-      match args with
-	|[] -> ()
-	|h::t -> print "OTHERFLAGS=";
-	  print h;
-	  List.iter (fun s -> print " ";print s) t;
-	  print "\n";
-    end;
-    (* Coq executables and relative variables *)
-    if !some_vfile || !some_mlpackfile || !some_mllibfile then
-      print "COQDEP?=\"$(COQBIN)coqdep\" -c\n";
-    if !some_vfile then begin
-    print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
-    print "COQCHKFLAGS?=-silent -o\n";
-    print "COQDOCFLAGS?=-interpolate -utf8\n";
-    print "COQC?=$(TIMER) \"$(COQBIN)coqc\"\n";
-    print "GALLINA?=\"$(COQBIN)gallina\"\n";
-    print "COQDOC?=\"$(COQBIN)coqdoc\"\n";
-    print "COQCHK?=\"$(COQBIN)coqchk\"\n";
-    print "COQMKTOP?=\"$(COQBIN)coqmktop\"\n\n";
-    end;
-    (* Caml executables and relative variables *)
-    if !some_ml4file || !some_mlfile || !some_mlifile then begin
-    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";
-    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n";
-    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
-    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
-    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n";
-    print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n";
-    print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
-    print "GRAMMARS?=grammar.cma\n";
-    print "ifeq ($(CAMLP4),camlp5)
-CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
-else
-CAMLP4EXTEND=
-endif\n";
-    print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\
-  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
-    end;
-    match is_install with
-      | Project_file.NoInstall -> ()
-      | Project_file.UnspecInstall ->
-        section "Install Paths.";
-	print "ifdef USERINSTALL\n";
-        print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
-        print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
-        print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n";
-	print "else\n";
-        print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n";
-        print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
-        print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
-	print "endif\n\n"
-      | Project_file.TraditionalInstall ->
-          section "Install Paths.";
-          print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n";
-          print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
-          print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
-          print "\n"
-      | Project_file.UserInstall ->
-          section "Install Paths.";
-          print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
-          print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
-          print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n";
-          print "COQTOPINSTALL=$(XDG_DATA_HOME)/coq/toploop\n";
-          print "\n"
-
-let parameters () =
-  print ".DEFAULT_GOAL := all\n\n";
-  print "# This Makefile may take arguments passed as environment variables:\n";
-  print "# COQBIN to specify the directory where Coq binaries resides;\n";
-  print "# TIMECMD set a command to log .v compilation time;\n";
-  print "# TIMED if non empty, use the default time command as TIMECMD;\n";
-  print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n";
-  print "# DSTROOT to specify a prefix to install path.\n";
-  print "# VERBOSE to disable the short display of compilation rules.\n\n";
-  print "VERBOSE?=\n";
-  print "SHOW := $(if $(VERBOSE),@true \"\",@echo \"\")\n";
-  print "HIDE := $(if $(VERBOSE),,@)\n\n";
-  print "# Here is a hack to make $(eval $(shell works:\n";
-  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 "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
-  print "vo_to_obj = $(addsuffix .o,\\\n";
-  print "  $(filter-out Warning: Error:,\\\n";
-  print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
-
-let include_dirs (inc_ml,inc_q,inc_r) =
-  let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
-  let includes =
-    List.map (fun (p,l,_) ->
-              let l' = if l = "" then "\"\"" else l in
-              " \"" ^ p ^ "\" " ^ l' ^"") in
-  let str_ml = parse_ml_includes inc_ml in
-  section "Libraries definitions.";
-  if !some_ml4file || !some_mlfile || !some_mlifile then begin
-    print "OCAMLLIBS?="; print_list "\\\n  " str_ml; print "\n";
-  end;
-  if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
-    print "COQLIBS?=";
-    print_prefix_list "\\\n  -Q" (includes inc_q);
-    print_prefix_list "\\\n  -R" (includes inc_r);
-    print_prefix_list "\\\n  " str_ml;
-    print "\n";
-  end;
-  if !some_vfile then begin
-    print "COQCHKLIBS?=";
-    print_prefix_list "\\\n  -R" (includes inc_q);
-    print_prefix_list "\\\n  -R" (includes inc_r);
-    print "\n";
-    print "COQDOCLIBS?=";
-    print_prefix_list "\\\n  -R" (includes inc_q);
-    print_prefix_list "\\\n  -R" (includes inc_r);
-    print "\n";
+  match candidates with
+  | [] ->
+     (* BACKWARD COMPATIBILITY: -I into the only logical root *)
+     begin match
+        r_includes,
+        List.find (fun {thing={ canonical_path = p }} -> is_prefix p file_dir)
+          ml_includes
+     with
+        | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} ->
+            let destination =
+              clean_path (physical_dir_of_logical_dir logic ^ "/" ^
+                          chop_prefix p file_dir ^ "/") in
+            Printf.printf "%s" (quote destination)
+        | _ -> () (* skip *)
+        | exception Not_found -> () (* skip *)
+     end
+  | [s] -> Printf.printf "%s" (quote s)
+  | _ -> assert false
+
+let share_prefix s1 s2 =
+  let s1 = CString.split '.' s1 in
+  let s2 = CString.split '.' s2 in
+  match s1, s2 with
+  | x :: _ , y :: _ -> x = y
+  | _ -> false
+
+let _ =
+  let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
+  let prog, args =
+    let args = Array.to_list Sys.argv in
+    let prog = List.hd args in
+    prog, List.tl args in
+
+  let only_destination, args = match args with
+    | "-destination-of" :: tgt :: rest -> Some tgt, rest
+    | _ -> None, args in
+
+  let project = 
+    try cmdline_args_to_project ~curdir:Filename.current_dir_name args
+    with Parsing_error s -> prerr_endline s; usage_coq_makefile () in
+
+  if only_destination <> None then begin
+    destination_of project (Option.get only_destination);
+    exit 0
   end;
-  print "\n"
 
-let double_colon = ["clean"; "cleanall"; "archclean"]
+  if project.makefile = None then
+    eprintf "Warning: Omitting -o is deprecated\n\n";
+    (* We want to know the name of the Makefile (say m) in order to
+     * generate m.conf and include m.local *)
 
-let custom sps =
-  let pr_path (file,dependencies,is_phony,com) =
-    print file;
-    print (if List.mem file double_colon then ":: " else ": ");
-    print dependencies; print "\n";
-    if com <> "" then (print "\t"; print com; print "\n");
-    print "\n"
-  in
-    if sps <> [] then section "Custom targets.";
-    List.iter pr_path sps
+  let conf_file = Option.default "CoqMakefile" project.makefile ^ ".conf" in
+  let local_file = Option.default "CoqMakefile" project.makefile ^ ".local" in
 
-let subdirs sds =
-  let pr_subdir s =
-    print s; print ":\n\t+cd \""; print s; print "\" && $(MAKE) all\n\n"
-  in
-  if sds <> [] then
-    let () =
-      Format.eprintf "@[Warning: Targets for subdirectories are very fragile.@ " in
-    let () =
-      Format.eprintf "For example,@ nothing is done to handle dependencies@ with them.@]@." in
-      section "Subdirectories.";
-    List.iter pr_subdir sds
-
-let forpacks l =
-  let () = if l <> [] then section "Ad-hoc implicit rules for mlpack." in
-  List.iter (fun it ->
-    let h = Filename.chop_extension it in
-    let pk = String.capitalize (Filename.basename h) in
-    printf "$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml\n" h;
-    printf "\t$(SHOW)'CAMLOPT -c -for-pack %s $<'\n" pk;
-    printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" pk;
-    printf "$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml4\n" h;
-    printf "\t$(SHOW)'CAMLOPT -c -pp -for-pack %s $<'\n" pk;
-    printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" pk
-  ) l
-
-let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other_targets inc =
-  let decl_var var = function
-    |[] -> ()
-    |l ->
-      printf "%s:=" var; print_list "\\\n  " l; print "\n\n";
-      print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n";
-      printf "-include $(addsuffix .d,$(%s))\n" var;
-      print "else\nifeq ($(MAKECMDGOALS),)\n";
-      printf "-include $(addsuffix .d,$(%s))\n" var;
-      print "endif\nendif\n\n";
-      printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var
-  in
-  section "Files dispatching.";
-  decl_var "VFILES" vfiles;
-  begin match vfiles with
-    |[] -> ()
-    |l ->
-      print "VO=vo\n";
-      print "VOFILES:=$(VFILES:.v=.$(VO))\n";
-      classify_files_by_root "VOFILES" l inc;
-      print "GLOBFILES:=$(VFILES:.v=.glob)\n";
-      print "GFILES:=$(VFILES:.v=.g)\n";
-      print "HTMLFILES:=$(VFILES:.v=.html)\n";
-      print "GHTMLFILES:=$(VFILES:.v=.g.html)\n";
-      print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n";
-      print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
-      print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n";
-      classify_files_by_root "NATIVEFILES" l inc
+  if project.extra_targets <> [] then begin
+    eprintf "Warning: -extra and -extra-phony are deprecated.\n";
+    eprintf "Warning: Write the extra targets in %s.\n\n" local_file;
   end;
-  decl_var "ML4FILES" ml4files;
-  decl_var "MLFILES" mlfiles;
-  decl_var "MLPACKFILES" mlpackfiles;
-  decl_var "MLLIBFILES" mllibfiles;
-  decl_var "MLIFILES" mlifiles;
-  let mlsfiles = match ml4files,mlfiles,mlpackfiles with
-    |[],[],[] -> []
-    |[],[],_ -> Printf.eprintf "Mlpack cannot work without ml[4]?"; []
-    |[],ml,[] ->
-      print "ALLCMOFILES:=$(MLFILES:.ml=.cmo)\n";
-      ml
-    |ml4,[],[] ->
-      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo)\n";
-      ml4
-    |ml4,ml,[] ->
-      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n";
-      List.rev_append ml ml4
-    |[],ml,mlpack ->
-      print "ALLCMOFILES:=$(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
-      List.rev_append mlpack ml
-    |ml4,[],mlpack ->
-      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
-      List.rev_append mlpack ml4
-    |ml4,ml,mlpack ->
-      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
-      List.rev_append mlpack (List.rev_append ml ml4) in
-  begin match mlsfiles with
-    |[] -> ()
-    |l ->
-  print "CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))\n";
-      classify_files_by_root "CMOFILES" l inc;
-      print "CMXFILES=$(CMOFILES:.cmo=.cmx)\n";
-      print "OFILES=$(CMXFILES:.cmx=.o)\n";
-  end;
-  begin match mllibfiles with
-    |[] -> ()
-    |l ->
-      print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n";
-	classify_files_by_root "CMAFILES" l inc;
-      print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n";
-  end;
-  begin match mlifiles,mlsfiles with
-    |[],[] -> ()
-    |l,[] ->
-       print "CMIFILES:=$(MLIFILES:.mli=.cmi)\n";
-	classify_files_by_root "CMIFILES" l inc;
-    |[],l ->
-      print "CMIFILES=$(ALLCMOFILES:.cmo=.cmi)\n";
-      classify_files_by_root "CMIFILES" l inc;
-    |l1,l2 ->
-      print "CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n";
-      classify_files_by_root "CMIFILES" (l1@l2) inc;
+
+  if project.subdirs <> [] then begin
+    eprintf "Warning: Subdirectories are deprecated.\n";
+    eprintf "Warning: Use double colon rules in %s.\n\n" local_file;
   end;
-  begin match mllibfiles,mlsfiles with
-    |[],[] -> ()
-    |l,[] ->
-      print "CMXSFILES:=$(CMXAFILES:.cmxa=.cmxs)\n";
-      classify_files_by_root "CMXSFILES" l inc;
-    |[],l ->
-      print "CMXSFILES=$(CMXFILES:.cmx=.cmxs)\n";
-      classify_files_by_root "CMXSFILES" l inc;
-    |l1,l2 ->
-      print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n";
-      classify_files_by_root "CMXSFILES" (l1@l2) inc;
+
+  let project = ensure_root_dir project in
+  
+  if project.install_kind <> (Some CoqProject_file.NoInstall) then begin
+    warn_install_at_root_directory project;
   end;
-  print "ifeq '$(HASNATDYNLINK)' 'true'\n";
-  print "HASNATDYNLINK_OR_EMPTY := yes\n";
-  print "else\n";
-  print "HASNATDYNLINK_OR_EMPTY :=\n";
-  print "endif\n\n";
-  section "Definition of the toplevel targets.";
-  print "all: ";
-  if !some_vfile then print "$(VOFILES) ";
-  if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) ";
-  if !some_mllibfile then print "$(CMAFILES) ";
-  if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile
-  then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) ";
-  print_list "\\\n  " other_targets; print "\n\n";
-  if !some_mlifile then
-    begin
-      print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
-      print "\t mkdir $@ || rm -rf $@/*\n";
-      print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
-      print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
-      print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
-    end;
-  if !some_vfile then
-    begin
-      print "quick: $(VOFILES:.vo=.vio)\n\n";
-      print "vio2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)\n";
-      print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)\n";
-      print "gallina: $(GFILES)\n\n";
-      print "html: $(GLOBFILES) $(VFILES)\n";
-      print "\t- mkdir -p html\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
-      print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
-      print "\t- mkdir -p html\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
-      print "all.ps: $(VFILES)\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
-      print "all-gal.ps: $(VFILES)\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
-      print "all.pdf: $(VFILES)\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
-      print "all-gal.pdf: $(VFILES)\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
-      print "validate: $(VOFILES)\n";
-      print "\t$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))\n\n";
-      print "beautify: $(VFILES:=.beautified)\n";
-      print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n";
-      print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n";
-      print "\t@echo \'If there were a problem, execute \"for file in $$(find . -name \\*.v.old -print); do mv $${file} $${file%.old}; done\" in your shell/'\n\n"
-    end
-
-let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
-  let other_targets =
-    CList.map_filter
-      (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None)
-      sps @ sds in
-  main_targets vfiles mlfiles other_targets inc;
-  print ".PHONY: ";
-  print_list
-    " "
-    ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall"
-     :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-doc"
-     :: "install-natdynlink" :: "install-toploop" :: "opt" :: "printenv"
-     :: "quick" :: "uninstall" :: "userinstall" :: "validate" :: "vio2vo"
-     :: (sds@(CList.map_filter
-		(fun (n,_,is_phony,_) ->
-		 if is_phony then Some n else None) sps)));
-  print "\n\n";
-  custom sps;
-  subdirs sds;
-  forpacks mlpackfiles
-
-let banner () =
-  print (Printf.sprintf
-"#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \\VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V%s ##
-#############################################################################
-
-" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
-
-let warning () =
-  print "# WARNING\n#\n";
-  print "# This Makefile has been automagically generated\n";
-  print "# Edit at your own risks !\n";
-  print "#\n# END OF WARNING\n\n"
-
-let print_list l = List.iter (fun x -> print x; print " ") l
-
-let command_line args =
-  print "#\n# This Makefile was generated by the command line :\n";
-  print "# coq_makefile ";
-  print_list args;
-  print "\n#\n\n"
-
-let ensure_root_dir (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc =
-  let (ml_inc,i_inc,r_inc) = inc in
-  let here = Sys.getcwd () in
-  let not_tops =  List.for_all (fun s -> s <> Filename.basename s) in
-  if List.exists (fun (_,_,x) -> x = here) i_inc
-    || List.exists (fun (_,_,x) -> is_prefix x here) r_inc
-    || (not_tops vfiles && not_tops mlis && not_tops ml4s && not_tops mls
-	&& not_tops mllibs && not_tops mlpacks)
-  then
-    inc
-  else
-    ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc)
-
-let warn_install_at_root_directory (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc =
-  let (inc_ml,inc_i,inc_r) = inc in
-  let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") (inc_r@inc_i) in
-  let inc_top_p = List.map (fun (p,_,_) -> p) inc_top in
-  let files = vfiles @ mlis @ ml4s @ mls @ mllibs @ mlpacks in
-  if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files
-  then
-    Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R or -Q %sis recommended\n"
-      (if inc_top = [] then "" else "with non trivial logical root ")
 
-let check_overlapping_include (_,inc_i,inc_r) =
-  let pwd = Sys.getcwd () in
-  let aux = function
-    | [] -> ()
-    | (pdir,_,abspdir)::l ->
-	if not (is_prefix pwd abspdir) then
-	  Printf.eprintf "Warning: in option -R/-Q, %s is not a subdirectory of the current directory\n" pdir;
-	List.iter (fun (pdir',_,abspdir') ->
-	  if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then
-	    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
-    |_::_ -> var := true in
-  let (project_file,makefile,is_install,opt),l =
-    try
-      Project_file.process_cmd_line Filename.current_dir_name
-       (None,None,Project_file.UnspecInstall,true) [] args
-    with Project_file.Parsing_error -> usage () in
-  let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs =
-    Project_file.split_arguments l in
-
-  let () = match project_file with |None -> () |Some f -> make_name := f in
-  let () = match makefile with
-    |None -> ()
-    |Some f -> makefile_name := f; output_channel := open_out f in
-  has_file some_vfile v_f; has_file some_mlifile mli_f;
-  has_file some_mlfile ml_f; has_file some_ml4file ml4_f;
-  has_file some_mllibfile mllib_f; has_file some_mlpackfile mlpack_f;
-  let check_dep f =
-    if Filename.check_suffix f ".v" then some_vfile := true
-    else if (Filename.check_suffix f ".mli") then some_mlifile := true
-    else if (Filename.check_suffix f ".ml4") then some_ml4file := true
-    else if (Filename.check_suffix f ".ml") then some_mlfile := true
-    else if (Filename.check_suffix f ".mllib") then some_mllibfile := true
-    else if (Filename.check_suffix f ".mlpack") then some_mlpackfile := true
-  in
-  List.iter (fun (_,dependencies,_,_) ->
-    List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps;
+  check_overlapping_include project;
 
-  let inc = ensure_root_dir targets inc in
-  if is_install <> Project_file.NoInstall then begin
-    warn_install_at_root_directory targets inc;
-  end;
-  check_overlapping_include inc;
-  banner ();
-  header_includes ();
-  warning ();
-  command_line args;
-  parameters ();
-  include_dirs inc;
-  variables is_install opt defs;
-  all_target targets inc;
-  section "Special targets.";
-  standard opt;
-  install targets inc is_install;
-  merlin targets inc;
-  clean sds sps;
-  make_makefile sds;
-  implicit ();
-  warning ();
-  if not (makefile = None) then close_out !output_channel;
+  Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1);
+  
+  let ocm = Option.cata open_out stdout project.makefile in
+  generate_makefile ocm conf_file local_file (prog :: args) project;
+  close_out ocm;
+  let occ = open_out conf_file in
+  generate_conf occ project (prog :: args);
+  close_out occ;
   exit 0
 
-let _ =
-  let args =
-    if Array.length Sys.argv = 1 then usage ();
-    List.tl (Array.to_list Sys.argv)
-  in
-    do_makefile args
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index e17011b3..0ffa5bd7 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* coq-tex
diff --git a/tools/coqc.ml b/tools/coqc.ml
index b12d4871..90d8e67c 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Coq compiler : coqc *)
@@ -77,25 +79,28 @@ let parse_args () =
     | ("-v"|"--version") :: _ -> Usage.version 0
 
     | ("-where") :: _ ->
-        Envars.set_coqlib (fun x -> x);
+        Envars.set_coqlib ~fail:(fun x -> x);
         print_endline (Envars.coqlib ());
         exit 0
 
     | ("-config" | "--config") :: _ ->
-        Envars.set_coqlib (fun x -> x);
-        Usage.print_config ();
+        Envars.set_coqlib ~fail:(fun x -> x);
+        Envars.print_config stdout Coq_config.all_src_dirs;
         exit 0
+      
+    | ("-print-version" | "--print-version") :: _ ->
+        Usage.machine_readable_version 0
 
 (* Options for coqtop : a) options with 0 argument *)
 
-    | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
+    | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
       |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
-      |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
-      |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
-      |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
+      |"-q"|"-profile"|"-echo" |"-quiet"
+      |"-silent"|"-m"|"-beautify"|"-strict-implicit"
       |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
+      |"-stm-debug"
       as o) :: rem ->
 	parse (cfiles,o::args) rem
 
@@ -106,7 +111,7 @@ let parse_args () =
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
-      |"-o"|"-profile-ltac-cutoff" 
+      |"-o"|"-profile-ltac-cutoff"|"-mangle-names"
       as o) :: rem ->
 	begin
 	  match rem with
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a7c32e1d..12b5cab0 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Printf
@@ -320,19 +322,25 @@ let treat_coq_file chan =
         List.fold_left (fun accu v -> mark_v_done from accu v) acc strl
       | Declare sl ->
         let declare suff dir s =
-          let base = file_name s dir in
-          let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in
-          (escape base, suff ^ opt)
+          let base = escape (file_name s dir) in
+          match !option_dynlink with
+          | No -> []
+          | Byte -> [base,suff]
+          | Opt -> [base,".cmxs"]
+          | Both -> [base,suff; base,".cmxs"]
+          | Variable ->
+             if suff=".cmo" then [base,"$(DYNOBJ)"]
+             else [base,"$(DYNLIB)"]
         in
         let decl acc str =
           let s = basename_noext str in
           if not (StrSet.mem s !deja_vu_ml) then
             let () = deja_vu_ml := StrSet.add s !deja_vu_ml in
             match search_mllib_known s with
-            | Some mldir -> (declare ".cma" mldir s) :: acc
+            | Some mldir -> (declare ".cma" mldir s) @ acc
             | None ->
               match search_ml_known s with
-              | Some mldir -> (declare ".cmo" mldir s) :: acc
+              | Some mldir -> (declare ".cmo" mldir s) @ acc
               | None -> acc
           else acc
         in
@@ -435,9 +443,10 @@ let usage () =
      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 "  -boot : For coq developers, 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 "  -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.";
   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? *)
@@ -449,10 +458,24 @@ let usage () =
   eprintf "  -coqlib dir : set the coq standard library directory\n";
   eprintf "  -suffix s : \n";
   eprintf "  -slash : deprecated, no effect\n";
+  eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n";
   exit 1
 
 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 add_r_include path l = add_rec_dir_import add_known path (split_period l)
+
+let treat_coqproject f =
+  let open CoqProject_file in
+  let iter_sourced f = List.iter (fun {thing} -> f thing) in
+  let project = read_project_file f in
+  iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes;
+  iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes;
+  iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes;
+  iter_sourced (fun f -> treat_file None f) (all_files project)
+
 let rec parse = function
   | "-c" :: ll -> option_c := true; parse ll
   | "-D" :: ll -> option_D := true; parse ll
@@ -460,10 +483,11 @@ 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
+  | "-f" :: f :: ll -> treat_coqproject f; parse ll
   | "-I" :: r :: ll -> add_caml_dir r; parse ll
   | "-I" :: [] -> usage ()
-  | "-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" :: r :: ln :: ll -> add_r_include r ln; parse ll
+  | "-Q" :: r :: ln :: ll -> add_q_include r 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
@@ -476,17 +500,22 @@ let rec parse = function
   | "-slash" :: ll ->
     Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
     parse ll
+  | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+  | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+  | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+  | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+  | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
   | ("-h"|"--help"|"-help") :: _ -> usage ()
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
+  if not Coq_config.has_natdynlink then option_dynlink := No;
   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_import add_known "theories" ["Coq"];
@@ -495,14 +524,14 @@ let coqdep () =
     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:CErrors.error;
+    Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
     let coqlib = Envars.coqlib () in
     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_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 -> Feedback.msg_warning (Pp.str x)));
+      (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x)));
     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;
@@ -526,5 +555,5 @@ let _ =
   try
     coqdep ()
   with CErrors.UserError(s,p) ->
-    let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
-    Feedback.msg_error pp
+    let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p))  in
+    Format.eprintf "%a@\n%!" Pp.pp_with pp
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 6fc82683..aa023e69 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Coqdep_common
@@ -16,7 +18,11 @@ open Coqdep_common
 *)
 
 let rec parse = function
-  | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
+  | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+  | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+  | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+  | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+  | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
   | "-mldep" :: ocamldep :: ll ->
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0064aebd..db69a3b7 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Printf
@@ -15,7 +17,7 @@ open Minisys
     behavior is the one of [coqdep -boot]. Its only dependencies
     are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so.
     If it need someday some additional information, pass it via
-    options (see for instance [option_natdynlk] below).
+    options (see for instance [option_dynlink] below).
 *)
 
 module StrSet = Set.Make(String)
@@ -26,9 +28,11 @@ module StrListMap = Map.Make(StrList)
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
+type dynlink = Opt | Byte | Both | No | Variable
+
 let option_c = ref false
 let option_noglob = ref false
-let option_natdynlk = ref true
+let option_dynlink = ref Both
 let option_boot = ref false
 let option_mldep = ref None
 
@@ -36,6 +40,10 @@ let norec_dirs = ref StrSet.empty
 
 let suffixe = ref ".vo"
 
+[@@@ocaml.warning "-3"]       (* String.capitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+[@@@ocaml.warning "+3"]
+
 type dir = string option
 
 (** [get_extension f l] checks whether [f] has one of the extensions
@@ -94,8 +102,18 @@ let safe_hash_add cmp clq q (k, (v, b)) =
     For the ML files, the string is the basename without extension.
 *)
 
+let same_path_opt s s' =
+  let nf s = (* ./foo/a.ml and foo/a.ml are the same file *)
+    if Filename.is_implicit s
+    then "." // s
+    else s
+  in
+  let s = match s with None -> "." | Some s -> nf s in
+  let s' = match s' with None -> "." | Some s' -> nf s' in
+  s = s'
+
 let warning_ml_clash x s suff s' suff' =
-  if suff = suff' then
+  if suff = suff' && not (same_path_opt s s') then
   eprintf
     "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
     (match s with None -> "." | Some d -> d)
@@ -219,7 +237,6 @@ let register_dir_logpath,find_dir_logpath =
 
 let file_name s = function
   | None     -> s
-  | Some "." -> s
   | Some d   -> d // s
 
 let depend_ML str =
@@ -293,15 +310,15 @@ let traite_fichier_modules md ext =
       (fun a_faire str -> match search_mlpack_known str with
 	| Some mldir ->
 	  let file = file_name str mldir in
-	  a_faire^" "^file
+          a_faire @ [file]
 	| None ->
 	  match search_ml_known str with
 	    | Some mldir ->
 	      let file = file_name str mldir in
-	      a_faire^" "^file
-	    | None -> a_faire) "" list
+              a_faire @ [file]
+            | None -> a_faire) [] list
   with
-    | Sys_error _ -> ""
+    | Sys_error _ -> []
     | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j)
 
 (* Makefile's escaping rules are awful: $ is escaped by doubling and
@@ -380,10 +397,16 @@ let rec traite_fichier_Coq suffixe verbose f =
        		end) strl
 	  | Declare sl ->
 	      let declare suff dir s =
-		let base = file_name s dir in
-		let opt = if !option_natdynlk then " "^base^".cmxs" else "" in
-		printf " %s%s%s" (escape base) suff opt
-	      in
+		let base = escape (file_name s dir) in
+                match !option_dynlink with
+                | No -> ()
+                | Byte -> printf " %s%s" base suff
+                | Opt -> printf " %s.cmxs" base
+                | Both -> printf " %s%s %s.cmxs" base suff base
+                | Variable ->
+                   printf " %s%s" base
+                    (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")
+              in
 	      let decl str =
                 let s = basename_noext str in
 		if not (StrSet.mem s !deja_vu_ml) then begin
@@ -443,7 +466,7 @@ let mL_dependencies () =
        let fullname = file_name name dirname in
        let dep = traite_fichier_modules fullname ".mllib" in
        let efullname = escape fullname in
-       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep;
+       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
        printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
        printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
        flush stdout)
@@ -453,9 +476,13 @@ let mL_dependencies () =
        let fullname = file_name name dirname in
        let dep = traite_fichier_modules fullname ".mlpack" in
        let efullname = escape fullname in
-       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep;
+       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
        printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
        printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
+       let efullname_capital = capitalize (Filename.basename efullname) in
+       List.iter (fun dep ->
+         printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
+         dep;
        flush stdout)
     (List.rev !mlpackAccu)
 
@@ -544,13 +571,6 @@ let add_rec_dir_no_import add_file 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 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 false add_caml_known phys_dir []
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 633c474a..d0d79324 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 module StrSet : Set.S with type elt = string
@@ -19,7 +21,10 @@ val find_dir_logpath: string -> string list
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
-val option_natdynlk : bool ref
+
+type dynlink = Opt | Byte | Both | No | Variable
+
+val option_dynlink : dynlink ref
 val option_mldep : string option ref
 val norec_dirs : StrSet.t ref
 val suffixe : string ref
@@ -64,8 +69,5 @@ val add_rec_dir_no_import :
 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 bb17fdf9..0e2b332f 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 type mL_token = Use_module of string
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index eb233b8f..ade5e5be 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 {
@@ -25,8 +27,6 @@
   exception Fin_fichier
   exception Syntax_error of int*int
 
-  let field_name s = String.sub s 1 (String.length s - 1)
-
   let unquote_string s =
     String.sub s 1 (String.length s - 2)
 
@@ -39,30 +39,33 @@
 
   let syntax_error lexbuf =
     raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+
+  let check_valid lexbuf s =
+    match Unicode.ident_refutation s with
+    | None -> s
+    | Some _ -> syntax_error lexbuf
+
+  let get_ident lexbuf =
+    let s = Lexing.lexeme lexbuf in check_valid lexbuf s
+
+  let get_field_name lexbuf =
+    let s = Lexing.lexeme lexbuf in
+    check_valid lexbuf (String.sub s 1 (String.length s - 1))
+
+  [@@@ocaml.warning "-3"]       (* String.uncapitalize_ascii since 4.03.0 GPR#124 *)
+  let uncapitalize = String.uncapitalize
+  [@@@ocaml.warning "+3"]
 }
 
 let space = [' ' '\t' '\n' '\r']
-let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
-let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
-let identchar =
-  ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let lowercase = ['a'-'z']
+let uppercase = ['A'-'Z']
+let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9']
 let caml_up_ident = uppercase identchar*
 let caml_low_ident = lowercase identchar*
 
-let coq_firstchar =
-  (* This is only an approximation, refer to lib/util.ml for correct def *)
-  ['A'-'Z' 'a'-'z' '_'] |
-  (* superscript 1 *)
-  '\194' '\185' |
-  (* utf-8 latin 1 supplement *)
-  '\195' ['\128'-'\150'] | '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] |
-  (* utf-8 letters *)
-  '\206' (['\145'-'\161'] | ['\163'-'\187'])
-  '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
-    | '\129' [ '\176'-'\187' ] (* superscripts *)
-    | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
-let coq_identchar = coq_firstchar | ['\'' '0'-'9']
-let coq_ident = coq_firstchar coq_identchar*
+(* This is an overapproximation, we check correctness afterwards *)
+let coq_ident = ['A'-'Z' 'a'-'z' '_' '\128'-'\255'] ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9' '\128'-'\255']*
 let coq_field = '.' coq_ident
 
 let dot = '.' ( space+ | eof)
@@ -70,7 +73,9 @@ let dot = '.' ( space+ | eof)
 rule coq_action = parse
   | "Require" space+
       { require_modifiers None lexbuf }
-  | "Local"? "Declare" space+ "ML" space+ "Module" space+
+  | "Local" space+ "Declare" space+ "ML" space+ "Module" space+
+      { modules [] lexbuf }
+  | "Declare" space+ "ML" space+ "Module" space+
       { modules [] lexbuf }
   | "Load" space+
       { load_file lexbuf }
@@ -97,7 +102,7 @@ and from_rule = parse
   | space+
       { from_rule lexbuf }
   | coq_ident
-      { let from = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+      { let from = coq_qual_id_tail [get_ident lexbuf] lexbuf in
         consume_require (Some from) lexbuf }
   | eof
       { syntax_error lexbuf }
@@ -154,7 +159,7 @@ and caml_action = parse
   | space +
       { caml_action lexbuf }
   | "open" space* (caml_up_ident as id)
-        { Use_module (String.uncapitalize id) }
+        { Use_module (uncapitalize id) }
   | "module" space+ caml_up_ident
         { caml_action lexbuf }
   | caml_low_ident { caml_action lexbuf }
@@ -236,7 +241,7 @@ and load_file = parse
 	parse_dot lexbuf;
 	Load (unquote_vfile_string s) }
   | coq_ident
-      { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
+      { let s = get_ident lexbuf in skip_to_dot lexbuf; Load s }
   | eof
       { syntax_error lexbuf }
   | _
@@ -248,7 +253,7 @@ and require_file from = parse
   | space+
       { require_file from lexbuf }
   | coq_ident
-      { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+      { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in
         let qid = coq_qual_id_list [name] lexbuf in
         parse_dot lexbuf;
         Require (from, qid) }
@@ -273,7 +278,7 @@ and coq_qual_id = parse
   | space+
       { coq_qual_id lexbuf }
   | coq_ident
-      { coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf }
+      { coq_qual_id_tail [get_ident lexbuf] lexbuf }
   | _
       { syntax_error lexbuf }
 
@@ -283,7 +288,7 @@ and coq_qual_id_tail module_name = parse
   | space+
       { coq_qual_id_tail module_name lexbuf }
   | coq_field
-      { coq_qual_id_tail (field_name (Lexing.lexeme lexbuf) :: module_name) lexbuf }
+      { coq_qual_id_tail (get_field_name lexbuf :: module_name) lexbuf }
   | eof
       { syntax_error lexbuf }
   | _
@@ -296,7 +301,7 @@ and coq_qual_id_list module_names = parse
   | space+
       { coq_qual_id_list module_names lexbuf }
   | coq_ident
-      { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+      { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in
         coq_qual_id_list (name :: module_names) lexbuf
       }
   | eof
@@ -321,12 +326,12 @@ and modules mllist = parse
 
 and qual_id ml_module_name = parse
   | '.' [^ '.' '(' '[']
-      { Use_module (String.uncapitalize ml_module_name) }
+      { Use_module (uncapitalize ml_module_name) }
   | eof { raise Fin_fichier }
   | _ { caml_action lexbuf }
 
 and mllib_list = parse
-  | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
+  | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf)
 		in s :: mllib_list lexbuf }
   | "*predef*" { mllib_list lexbuf }
   | space+ { mllib_list lexbuf }
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index f817ed5a..269c1a1d 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,14 +1,20 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Cdglobals
 
-let norm_char_latin1 c = match Char.uppercase c with
+[@@@ocaml.warning "-3"]       (* Char.uppercase_ascii since 4.03.0 GPR#124 *)
+let uppercase = Char.uppercase
+[@@@ocaml.warning "+3"]
+
+let norm_char_latin1 c = match uppercase c with
   | '\192'..'\198' -> 'A'
   | '\199' -> 'C'
   | '\200'..'\203' -> 'E'
@@ -19,19 +25,14 @@ let norm_char_latin1 c = match Char.uppercase c with
   | '\221' -> 'Y'
   | c -> c
 
-let norm_char_utf8 c = Char.uppercase c
+let norm_char_utf8 c = uppercase c
 
 let norm_char c =
   if !utf8 then norm_char_utf8 c else
   if !latin1 then norm_char_latin1 c else
-  Char.uppercase c
-
-let norm_string s =
-  let u = String.copy s in
-  for i = 0 to String.length s - 1 do
-    u.[i] <- norm_char s.[i]
-  done;
-  u
+  uppercase c
+
+let norm_string = String.map (fun s -> norm_char s)
 
 let compare_char c1 c2 = match norm_char c1, norm_char c2 with
   | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index f6d47a55..86303450 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Alphabetic order. *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5d48473d..0d3fb775 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 
@@ -70,23 +72,21 @@ let normalize_filename f =
   let dirname = Filename.dirname f in
   normalize_path dirname, basename
 
+(** Add a local installation suffix (unless the suffix is itself
+    absolute in which case the prefix does not matter) *)
+let use_suffix prefix suffix =
+  if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix
+
 (** A weaker analog of the function in Envars *)
 
 let guess_coqlib () =
   let file = "theories/Init/Prelude.vo" in
-  match Coq_config.coqlib with
-    | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
-    | Some _ | None ->
-      let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
-      let prefix = Filename.dirname coqbin in
-      let rpath =
-        if Coq_config.local then []
-        else if Coq_config.arch_is_win32 then ["lib"]
-        else ["lib/coq"]
-      in
-      let coqlib = List.fold_left (/) prefix rpath in
-      if Sys.file_exists (coqlib / file) then coqlib
-      else prefix
+  let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
+  let prefix = Filename.dirname coqbin in
+  let coqlib = use_suffix prefix Coq_config.coqlibsuffix in
+  if Sys.file_exists (coqlib / file) then coqlib else
+  if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file)
+  then Coq_config.coqlib else prefix
 
 let header_trailer = ref true
 let header_file = ref ""
diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli
new file mode 100644
index 00000000..2c9b3fb8
--- /dev/null
+++ b/tools/coqdoc/cdglobals.mli
@@ -0,0 +1,49 @@
+type target_language = LaTeX | HTML | TeXmacs | Raw
+val target_language : target_language ref
+type output_t = StdOut | MultFiles | File of string
+val output_dir : string ref
+val out_to : output_t ref
+val out_channel : out_channel ref
+val ( / ) : string -> string -> string
+val coqdoc_out : string -> string
+val open_out_file : string -> unit
+val close_out_file : unit -> unit
+type glob_source_t = NoGlob | DotGlob | GlobFile of string
+val glob_source : glob_source_t ref
+val normalize_path : string -> string
+val normalize_filename : string -> string * string
+val guess_coqlib : unit -> string
+val header_trailer : bool ref
+val header_file : string ref
+val header_file_spec : bool ref
+val footer_file : string ref
+val footer_file_spec : bool ref
+val quiet : bool ref
+val light : bool ref
+val gallina : bool ref
+val short : bool ref
+val index : bool ref
+val multi_index : bool ref
+val index_name : string ref
+val toc : bool ref
+val page_title : string ref
+val title : string ref
+val externals : bool ref
+val coqlib : string ref
+val coqlib_path : string ref
+val raw_comments : bool ref
+val parse_comments : bool ref
+val plain_comments : bool ref
+val toc_depth : int option ref
+val lib_name : string ref
+val lib_subtitles : bool ref
+val interpolate : bool ref
+val inline_notmono : bool ref
+val charset : string ref
+val inputenc : string ref
+val latin1 : bool ref
+val utf8 : bool ref
+val set_latin1 : unit -> unit
+val set_utf8 : unit -> unit
+type coq_module = string
+type file = Vernac_file of string * coq_module | Latex_file of string
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 58b19184..7732610f 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 919f37b9..1be440a7 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s Utility functions for the scanners *)
@@ -682,7 +684,7 @@ and doc_bol = parse
   | space* nl+
       { Output.paragraph (); doc_bol lexbuf }
   | "<<" space*
-      { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf }
   | eof
       { true }
   | '_'
@@ -707,7 +709,7 @@ and doc_list_bol indents = parse
       }
   | "<<" space*
       { Output.start_verbatim false;
-        verbatim false lexbuf;
+        verbatim 0 false lexbuf;
         doc_list_bol indents lexbuf }
   | "[[" nl
       { formatted := true;
@@ -852,7 +854,7 @@ and doc indents = parse
         Output.char (lexeme_char lexbuf 1);
         doc indents lexbuf }
   | "<<" space*
-      { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf }
   | '"'
       { if !Cdglobals.plain_comments 
 	then Output.char '"' 
@@ -892,13 +894,20 @@ and escaped_html = parse
         { backtrack lexbuf }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
-and verbatim inline = parse
+and verbatim depth inline = parse
   | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | ">>" { Output.stop_verbatim inline }
-  | "*)" { Output.stop_verbatim inline; backtrack lexbuf }
+  | "(*" { Output.verbatim_char inline '(';
+           Output.verbatim_char inline '*';
+           verbatim (depth+1) inline lexbuf }
+  | "*)" { if (depth == 0)
+           then (Output.stop_verbatim inline; backtrack lexbuf)
+           else (Output.verbatim_char inline '*';
+                 Output.verbatim_char inline ')';
+                 verbatim (depth-1) inline lexbuf) }
   | eof { Output.stop_verbatim inline }
-  | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
+  | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf }
 
 and url = parse
   | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 9be791a8..df493fdf 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Printf
@@ -117,7 +119,7 @@ let find_module m =
   if Hashtbl.mem local_modules m then
     Local
   else
-    try External (Filename.concat (find_external_library m) m)
+    try External (find_external_library m ^ "/" ^ m)
     with Not_found -> Unknown
 
 
@@ -155,10 +157,14 @@ let sort_entries el =
 
 let display_letter c = if c = '*' then "other" else String.make 1 c
 
+[@@@ocaml.warning "-3"]       (* String.lowercase_ascii since 4.03.0 GPR#124 *)
+let lowercase = String.lowercase
+[@@@ocaml.warning "+3"]
+
 let type_name = function
   | Library ->
       let ln = !lib_name in
-        if ln <> "" then String.lowercase ln else "library"
+        if ln <> "" then lowercase ln else "library"
   | Module -> "module"
   | Definition -> "definition"
   | Inductive -> "inductive"
@@ -197,7 +203,7 @@ let prepare_entry s = function
       let h = try String.index_from s 0 ':' with _ -> err () in
       let i = try String.index_from s (h+1) ':' with _ -> err () in
       let sc = String.sub s (h+1) (i-h-1) in
-      let ntn = String.make (String.length s - i) ' ' in
+      let ntn = Bytes.make (String.length s - i) ' ' in
       let k = ref 0 in
       let j = ref (i+1) in
       let quoted = ref false in
@@ -205,22 +211,22 @@ let prepare_entry s = function
       while !j <= l do
 	if not !quoted then begin
 	  (match s.[!j] with
-	  | '_' -> ntn.[!k] <- ' '; incr k
-	  | 'x' -> ntn.[!k] <- '_'; incr k
+	  | '_' -> Bytes.set ntn !k ' '; incr k
+	  | 'x' -> Bytes.set ntn !k '_'; incr k
 	  | '\'' -> quoted := true
 	  | _ -> assert false)
 	end
 	else
 	  if s.[!j] = '\'' then
 	    if (!j = l || s.[!j+1] = '_') then quoted := false
-	    else (incr j; ntn.[!k] <- s.[!j]; incr k)
+	    else (incr j; Bytes.set ntn !k s.[!j]; incr k)
 	  else begin
-	    ntn.[!k] <- s.[!j];
+	    Bytes.set ntn !k s.[!j];
 	    incr k
 	  end;
 	incr j
       done;
-      let ntn = String.sub ntn 0 !k in
+      let ntn = Bytes.sub_string ntn 0 !k in
       if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
   | _ ->
       s
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index e44bbd59..5cd30138 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Cdglobals
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index fe438738..11ec3d39 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 82d3d62b..d2522700 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Cdglobals
@@ -19,6 +21,10 @@ let printf s = Printf.fprintf !out_channel s
 
 let sprintf = Printf.sprintf
 
+[@@@ocaml.warning "-3"]       (* String.{capitalize,lowercase}_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+let lowercase = String.lowercase
+[@@@ocaml.warning "+3"]
 
 (*s Coq keywords *)
 
@@ -36,7 +42,7 @@ let is_keyword =
       "Hypothesis"; "Hypotheses";
       "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
       "Implicit"; "Import"; "Inductive";
-      "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
+      "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Locate"; "Ltac";
       "Module"; "Module Type"; "Declare Module"; "Include";
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
@@ -58,9 +64,9 @@ let is_keyword =
       (*i (* coq terms *) *)
       "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
-      "fix"; "cofix";
+      "fix"; "cofix"; "is";
       (* Ltac *)
-      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch";
+      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; "type"; "of"; "rec";
       (* Notations *)
       "level"; "associativity"; "no"
        ]
@@ -70,7 +76,7 @@ let is_tactic =
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
       "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
       "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
-      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
       "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
@@ -689,25 +695,21 @@ module Html = struct
     printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
 
   let ident s loc =
-    if is_keyword s then begin
-      printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
-    end else begin
-      try
-        match loc with
-        | None -> raise Not_found
-        | Some loc ->
-            reference (translate s) (Index.find (get_module false) loc)
-      with Not_found ->
-	if is_tactic s then
-	  printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
-	else
-	  if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
-	  then
-	    try reference (translate s) (Index.find_string (get_module false) s)
-	    with _ -> Tokens.output_tagged_ident_string s
-	  else
-	    Tokens.output_tagged_ident_string s
-    end
+    try
+      match loc with
+      | None -> raise Not_found
+      | Some loc ->
+         reference (translate s) (Index.find (get_module false) loc)
+    with Not_found ->
+      if is_tactic s then
+	printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
+      else if is_keyword s then
+        printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
+      else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then
+	try reference (translate s) (Index.find_string (get_module false) s)
+	with Not_found -> Tokens.output_tagged_ident_string s
+      else
+	Tokens.output_tagged_ident_string s
 
   let proofbox () = printf "<font size=-2>&#9744;</font>"
 
@@ -846,7 +848,7 @@ module Html = struct
 	if t = Library then
          let ln = !lib_name in
            if ln <> "" then
-	       "[" ^ String.lowercase ln ^ "]", m ^ ".html", t
+	       "[" ^ lowercase ln ^ "]", m ^ ".html", t
            else
 	       "[library]", m ^ ".html", t
 	else
@@ -864,7 +866,7 @@ module Html = struct
 
   (* Impression de la table d'index *)
   let print_index_table_item i =
-    printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
+    printf "<tr>\n<td>%s Index</td>\n" (capitalize i.idx_name);
     List.iter
       (fun (c,l) ->
 	 if l <> [] then
@@ -912,7 +914,7 @@ module Html = struct
     let print_table () = print_index_table all_index in
     let print_one_index i =
       if i.idx_size > 0 then begin
-	printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
+	printf "<hr/>\n<h1>%s Index</h1>\n" (capitalize i.idx_name);
 	all_letters i
       end
     in
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 853bc29a..a8a50d75 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Cdglobals
@@ -64,7 +66,6 @@ val keyword : string -> loc -> unit
 val ident : string -> loc option -> unit
 val sublexer : char -> loc -> unit
 val sublexer_in_doc : char -> unit
-val initialize : unit -> unit
 
 val proofbox : unit -> unit
 
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index b6a1057a..49f7ef2f 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Application of printing rules based on a dictionary specific to the
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index f07efedf..00db2ad3 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Type of dictionaries *)
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
deleted file mode 100644
index eaf938e8..00000000
--- a/tools/coqmktop.ml
+++ /dev/null
@@ -1,305 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(** {1 Coqmktop} *)
-
-(** coqmktop is a script to link Coq, analogous to ocamlmktop.
-   The command line contains options specific to coqmktop, options for the
-   Ocaml linker and files to link (in addition to the default Coq files). *)
-
-(** {6 Utilities} *)
-
-(** Split a string at each blank
-*)
-let split_list =
-  let spaces = Str.regexp "[ \t\n]+" in
-  fun str -> Str.split spaces str
-
-let (/) = Filename.concat
-
-(** Which user files do we support (and propagate to ocamlopt) ?
-*)
-let supported_suffix f = match CUnix.get_extension f with
-  | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true
-  | _ -> false
-
-(** From bytecode extension to native
-*)
-let native_suffix f = match CUnix.get_extension f with
-  | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx"
-  | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa"
-  | ".a" -> f
-  | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a")
-
-(** Transforms a file name in the corresponding Caml module name.
-*)
-let module_of_file name =
-  String.capitalize
-    (try Filename.chop_extension name with Invalid_argument _ -> name)
-
-(** Run a command [prog] with arguments [args].
-    We do not use [Sys.command] anymore, see comment in [CUnix.sys_command].
-*)
-let run_command prog args =
-  match CUnix.sys_command prog args with
-  | Unix.WEXITED 127 -> failwith ("no such command "^prog)
-  | Unix.WEXITED n -> n
-  | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n)
-  | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n)
-
-
-
-(** {6 Coqmktop options} *)
-
-let opt        = ref false
-let top        = ref false
-let echo       = ref false
-let no_start   = ref false
-
-let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
-let is_camlp5 = Coq_config.camlp4 = "camlp5"
-
-
-(** {6 Includes options} *)
-
-(** Since the Coq core .cma are given with their relative paths
-    (e.g. "lib/clib.cma"), we only need to include directories mentionned in
-    the temp main ml file below (for accessing the corresponding .cmi). *)
-
-let std_includes basedir =
-  let rebase d = match basedir with None -> d | Some base -> base / d in
-  ["-I"; rebase ".";
-   "-I"; rebase "lib";
-   "-I"; rebase "toplevel";
-   "-I"; rebase "kernel/byterun";
-   "-I"; Envars.camlp4lib () ] @
-  (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
-
-(** For the -R option, visit all directories under [dir] and add
-    corresponding -I to the [opts] option list (in reversed order) *)
-let incl_all_subdirs dir opts =
-  let l = ref opts in
-  let add f = l := f :: "-I" :: !l in
-  let rec traverse dir =
-    if Sys.file_exists dir && Sys.is_directory dir then
-      let () = add dir in
-      let subdirs = try Sys.readdir dir with any -> [||] in
-      Array.iter (fun f -> traverse (dir/f)) subdirs
-  in
-  traverse dir; !l
-
-
-(** {6 Objects to link} *)
-
-(** NB: dynlink is now always linked, it is used for loading plugins
-    and compiled vm code (see native-compiler). We now reject platforms
-    with ocamlopt but no dynlink.cmxa during ./configure, and give
-    instructions there about how to build a dummy dynlink.cmxa,
-    cf. dev/dynlink.ml. *)
-
-(** OCaml + CamlpX libraries *)
-
-let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
-let camlp4_libs = if is_camlp5 then ["gramlib.cma"] else ["camlp4lib.cma"]
-let libobjs = ocaml_libs @ camlp4_libs
-
-(** Toplevel objects *)
-
-let ocaml_topobjs =
-  if is_ocaml4 then
-    ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"]
-  else
-    ["toplevellib.cma"]
-
-let camlp4_topobjs =
-  if is_camlp5 then
-    ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
-  else
-    [ "Camlp4Top.cmo";
-      "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
-      "Camlp4Parsers/Camlp4OCamlParser.cmo";
-      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
-
-let topobjs = ocaml_topobjs @ camlp4_topobjs
-
-(** Coq Core objects *)
-
-let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts)
-let core_objs = split_list Tolink.core_objs
-let core_libs = split_list Tolink.core_libs
-
-(** Build the list of files to link and the list of modules names
-*)
-let files_to_link userfiles =
-  let top = if !top then topobjs else [] in
-  let modules = List.map module_of_file (top @ core_objs @ userfiles) in
-  let objs = libobjs @ top @ core_libs in
-  let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles
-  in (modules, objs')
-
-
-(** {6 Parsing of the command-line} *)
-
-let usage () =
-  prerr_endline "Usage: coqmktop <options> <ocaml options> files\
-\nFlags are:\
-\n  -coqlib dir    Specify where the Coq object files are\
-\n  -ocamlfind dir Specify where the ocamlfind binary is\
-\n  -camlp4bin dir Specify where the Camlp4/5 binaries are\
-\n  -o exec-file   Specify the name of the resulting toplevel\
-\n  -boot          Run in boot mode\
-\n  -echo          Print calls to external commands\
-\n  -opt           Compile in native code\
-\n  -top           Build Coq on a OCaml toplevel (incompatible with -opt)\
-\n  -R dir         Add recursively dir to OCaml search path\
-\n";
-  exit 1
-
-let parse_args () =
-  let rec parse (op,fl) = function
-    | [] -> List.rev op, List.rev fl
-
-    (* Directories *)
-    | "-coqlib" :: d :: rem ->
-	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
-    | "-ocamlfind" :: d :: rem ->
-	Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem
-    | "-camlp4bin" :: d :: rem ->
-	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
-    | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem
-    | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage ()
-
-    (* Boolean options of coqmktop *)
-    | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
-    | "-opt" :: rem -> opt := true ; parse (op,fl) rem
-    | "-top" :: rem -> top := true ; parse (op,fl) rem
-    | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem
-    | "-echo" :: rem -> echo := true ; parse (op,fl) rem
-    | ("-v8"|"-full" as o) :: rem ->
-	Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem
-
-    (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *)
-    | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
-        parse (o::op,fl) rem
-    | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
-	begin
-	  match rem' with
-	    | a :: rem -> parse (a::o::op,fl) rem
-	    | []       -> usage ()
-	end
-
-    | ("-h"|"-help"|"--help") :: _ -> usage ()
-    | f :: rem when supported_suffix f -> parse (op,f::fl) rem
-    | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1
-  in
-  parse ([],[]) (List.tl (Array.to_list Sys.argv))
-
-
-(** {6 Temporary main file} *)
-
-(** remove the temporary main file
-*)
-let clean file =
-  let rm f = if Sys.file_exists f then Sys.remove f in
-  let basename = Filename.chop_suffix file ".ml" in
-  if not !echo then begin
-    rm file;
-    rm (basename ^ ".o");
-    rm (basename ^ ".cmi");
-    rm (basename ^ ".cmo");
-    rm (basename ^ ".cmx")
-  end
-
-(** Initializes the kind of loading in the main program
-*)
-let declare_loading_string () =
-  if not !top then
-    "Mltop.remove ();;"
-  else
-    "begin try\
-\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
-\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
-\n         | Toploop.Directive_none f -> f ()\
-\n         | _ -> ()\
-\n       end\
-\n     with\
-\n       | Not_found -> ()\
-\n     end;;\
-\n\
-\n     let ppf = Format.std_formatter;;\
-\n     Mltop.set_top\
-\n       {Mltop.load_obj=\
-\n         (fun f -> if not (Topdirs.load_file ppf f)\
-\n                   then CErrors.error (\"Could not load plugin \"^f));\
-\n        Mltop.use_file=Topdirs.dir_use ppf;\
-\n        Mltop.add_dir=Topdirs.dir_directory;\
-\n        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
-\n"
-
-(** create a temporary main file to link
-*)
-let create_tmp_main_file modules =
-  let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
-  try
-    (* Add the pre-linked modules *)
-    output_string oc "List.iter Mltop.add_known_module [\"";
-    output_string oc (String.concat "\";\"" modules);
-    output_string oc "\"];;\n";
-    (* Initializes the kind of loading *)
-    output_string oc (declare_loading_string());
-    (* Start the toplevel loop *)
-    if not !no_start then output_string oc "Coqtop.start();;\n";
-    close_out oc;
-    main_name
-  with reraise ->
-    clean main_name; raise reraise
-
-
-(** {6 Main } *)
-
-let main () =
-  let (options, userfiles) = parse_args () in
-  (* Directories: *)
-  let () = Envars.set_coqlib ~fail:CErrors.error in
-  let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
-  (* Which ocaml compiler to invoke *)
-  let prog = if !opt then "opt" else "ocamlc" in
-  (* Which arguments ? *)
-  if !opt && !top then failwith "no custom toplevel in native code !";
-  let flags = if !opt then [] else Coq_config.vmbyteflags in
-  let topstart = if !top then [ "topstart.cmo" ] else [] in
-  let (modules, tolink) = files_to_link userfiles in
-  let main_file = create_tmp_main_file modules in
-  try
-    (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
-       - With the coq .cma, we MUST use the -linkall option. *)
-    let args =
-      "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @
-      (std_includes basedir) @ tolink @ [ main_file ] @ topstart
-    in
-    if !echo then begin
-      let command = String.concat " " (Envars.ocamlfind ()::prog::args) in
-      print_endline command;
-      print_endline
-	("(command length is " ^
-	    (string_of_int (String.length command)) ^ " characters)");
-      flush Pervasives.stdout
-    end;
-    let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in
-    clean main_file;
-    exitcode
-  with reraise -> clean main_file; raise reraise
-
-let pr_exn = function
-  | Failure msg -> msg
-  | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err
-  | any -> Printexc.to_string any
-
-let _ =
-  try exit (main ())
-  with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index b4fc738d..f0f13874 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* coqwc - counts the lines of spec, proof and comments in Coq sources
@@ -94,7 +96,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036"
 let stars = "(*" '*'* "*)"
 let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
 let proof_start =
-  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
+  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" space+ (['0' - '9'])+ | "Next" space+ "Obligation"
 let def_start =
   "Definition" | "Fixpoint" | "Instance"
 let proof_end =
@@ -239,6 +241,7 @@ let process_channel ch =
   if !skip_header then read_header lb;
   spec lb
 
+[@@@ocaml.warning "-52"]
 let process_file f =
   try
     let ch = open_in f in
@@ -251,6 +254,7 @@ let process_file f =
 	flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
     | Sys_error s ->
 	flush stdout; eprintf "coqwc: %s\n" s; flush stderr
+[@@@ocaml.warning "+52"]
 
 (*s Parsing of the command line. *)
 
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index d7bdf907..68aadcfc 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open CoqworkmgrApi
@@ -14,7 +16,7 @@ type party = {
           sock     : Unix.file_descr;
           cout     : out_channel;
   mutable tokens   : int;
-          priority : Flags.priority;
+          priority : priority;
 }
 
 let answer party msg =
@@ -42,10 +44,10 @@ end = struct
   let is_empty q = !q = []
   let rec split acc = function
     | [] -> List.rev acc, []
-    | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l
+    | (_, { priority = Low }) :: _ as l -> List.rev acc, l
     | x :: xs -> split (x :: acc) xs
   let push (_,{ priority } as item) q =
-    if priority = Flags.Low then q := !q @ [item]
+    if priority = Low then q := !q @ [item]
     else
       let high, low = split [] !q in
       q := high @ (item :: low)
@@ -72,10 +74,13 @@ let really_read_fd fd s off len =
 let raw_input_line fd =
   try
     let b = Buffer.create 80 in
-    let s = String.make 1 '\000' in
-    while s <> "\n" do
+    let s = Bytes.make 1 '\000' in
+    let endl = Bytes.of_string "\n" in
+    let endr = Bytes.of_string "\r" in
+    while Bytes.compare s endl <> 0 do
       really_read_fd fd s 0 1;
-      if s <> "\n" && s <> "\r" then Buffer.add_string b s;
+      if Bytes.compare s endl <> 0 && Bytes.compare s endr <> 0
+      then Buffer.add_bytes b s;
     done;
     Buffer.contents b
   with Unix.Unix_error _ -> raise End_of_file
@@ -145,7 +150,7 @@ let check_alive s =
   | Some s ->
       let cout = Unix.out_channel_of_descr s in
       set_binary_mode_out cout true;
-      output_string cout (print_request (Hello Flags.Low)); flush cout;
+      output_string cout (print_request (Hello Low)); flush cout;
       output_string cout (print_request Ping); flush cout;
       begin match Unix.select [s] [] [] 1.0 with
       | [s],_,_ ->
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 8fcca535..d48c6d0a 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
@@ -12,24 +14,15 @@ let error s =
   prerr_endline ("fake_id: error: "^s);
   exit 1
 
+let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
+
 type coqtop = {
   xml_printer : Xml_printer.t;
   xml_parser : Xml_parser.t;
 }
 
-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 (Richpp.repr content)
+let print_error msg =
+  Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -37,20 +30,15 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   Xml_printer.print coqtop.xml_printer xml_query;
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
-    match Xmlprotocol.is_message xml with
-    | Some (level, _loc, content) ->
-      logger level content;
+    if Xmlprotocol.is_feedback xml then
       loop ()
-    | None ->
-      if Xmlprotocol.is_feedback xml then
-        loop ()
-      else Xmlprotocol.to_answer call xml
+    else Xmlprotocol.to_answer call xml
   in
   let res = loop () in
   if print then prerr_endline (Xmlprotocol.pr_full_value call res);
   match res with
-  | 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
+  | Interface.Fail (_,_,s) when fail -> print_error s; exit 1
+  | Interface.Fail (_,_,s) as x      -> print_error s; x
   | x -> x
 
 let eval_call c q = ignore(base_eval_call c q)
@@ -186,7 +174,7 @@ let print_document () =
           Str.global_replace (Str.regexp "^[\n ]*") ""
       (if String.length s > 20 then String.sub s 0 17 ^ "..."
        else s) in
-  prerr_endline (Pp.string_of_ppcmds
+  pperr_endline (
     (Document.print doc
       (fun b state_id { name; text } ->
         Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
@@ -199,7 +187,7 @@ let print_document () =
 module GUILogic = struct
 
   let after_add = function
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
+    | Interface.Fail (_,_,s) -> print_error s; exit 1
     | Interface.Good (id, (Util.Inl (), _)) ->
         Document.assign_tip_id doc id
     | Interface.Good (id, (Util.Inr tip, _)) ->
@@ -211,7 +199,7 @@ module GUILogic = struct
   let at id id' _ = Stateid.equal id' id
   
   let after_edit_at (id,need_unfocus) = function
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
+    | Interface.Fail (_,_,s) -> print_error s; exit 1
     | Interface.Good (Util.Inl ()) ->
         if need_unfocus then Document.unfocus doc;
         ignore(Document.cut_at doc id);
@@ -261,16 +249,14 @@ let eval_print l coq =
       let to_id, need_unfocus = get_id id in
       after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
   | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
-      eval_call (query (phrase,tip_id())) coq
+      eval_call (query (0,(phrase,tip_id()))) coq
   | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
       let to_id, _ = get_id id in
-      eval_call (query (phrase, to_id)) coq
+      eval_call (query (0,(phrase, to_id))) coq
   | [ Tok(_,"WAIT") ] ->
-      let phrase = "Stm Wait." in
-      eval_call (query (phrase,tip_id())) coq
+      eval_call (wait ()) coq
   | [ Tok(_,"JOIN") ] ->
-      let phrase = "Stm JoinDocument." in
-      eval_call (query (phrase,tip_id())) coq
+      eval_call (status true) coq
   | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
       let to_id, _ = get_id id in
       if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
@@ -304,17 +290,31 @@ let usage () =
      (Filename.basename Sys.argv.(0))
      (Parser.print grammar))
 
-module Coqide = Spawn.Sync(struct end)
+module Coqide = Spawn.Sync ()
 
 let main =
-  Sys.set_signal Sys.sigpipe
+  if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
-  let coqtop_name, coqtop_args, input_file = match Sys.argv with
-    | [| _; f |] -> "coqtop",[|"-ideslave"|], f
+  let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
+  let coqtop_name = (* from ide/ideutils.ml *)
+    let prog_name = "fake_ide" in
+    let len_prog_name = String.length prog_name in
+    let fake_ide_path = Sys.executable_name in
+    let fake_ide_path_len = String.length fake_ide_path in
+    let pos = fake_ide_path_len - len_prog_name in
+    let rex = Str.regexp_string prog_name in
+    try
+      let i = Str.search_backward rex fake_ide_path pos in
+      String.sub fake_ide_path 0 i ^ "coqtop" ^
+      String.sub fake_ide_path (i + len_prog_name)
+        (fake_ide_path_len - i - len_prog_name) 
+    with Not_found -> assert false in
+  let coqtop_args, input_file = match Sys.argv with
+    | [| _; f |] -> Array.of_list def_args, f
     | [| _; f; ct |] ->
         let ct = Str.split (Str.regexp " ") ct in
-        List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f
+        Array.of_list (def_args @ ct), f
     | _ -> usage () in
   let inc = if input_file = "-" then stdin else open_in input_file in
   let coq =
@@ -334,7 +334,7 @@ let main =
   let finish () =
     match base_eval_call (Xmlprotocol.status true) coq with
     | Interface.Good _ -> exit 0
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) in
+    | Interface.Fail (_,_,s) -> print_error s; exit 1 in
   (* The main loop *)
   init ();
   while true do
diff --git a/tools/gallina-db.el b/tools/gallina-db.el
index baabebb1..9664f69f 100644
--- a/tools/gallina-db.el
+++ b/tools/gallina-db.el
@@ -163,7 +163,7 @@ for DB structure."
 
 (defun coq-sort-menu-entries (menu)
   (sort menu 
-	'(lambda (x y) (string< 
+	(lambda (x y) (string< 
 			(downcase (elt x 0)) 
 			(downcase (elt y 0))))))
 
diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el
index c25abece..662762b0 100644
--- a/tools/gallina-syntax.el
+++ b/tools/gallina-syntax.el
@@ -390,7 +390,7 @@
     ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary")
     ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t)
     ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t)
-    ("Definition goal" "defg" "Definition #:#.\n#\nSave." t);; careful
+    ("Definition goal" "defg" "Definition #:#.\n#\nQed." t);; careful
     ("Fact" "fct" "Fact # : #." t "Fact")
     ("Goal" nil "Goal #." t "Goal")
     ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma")
@@ -492,7 +492,6 @@
      ("Require" nil "Require #." t "Require")
      ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation")
      ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline")
-     ("Save" nil "Save." t "Save")
      ("Search" nil "Search #" nil "Search")
      ("SearchAbout" nil "SearchAbout #" nil "SearchAbout")
      ("SearchPattern" nil "SearchPattern #" nil "SearchPattern")
@@ -710,7 +709,6 @@ Used by `coq-goal-command-p'"
 
 (defvar coq-keywords-save-strict
   '("Defined"
-    "Save"
     "Qed"
     "End"
     "Admitted"
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 0bf98a8f..c7ff76be 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Gallina_lexer
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 449efd57..1a594aeb 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 {
@@ -105,7 +107,6 @@ and end_of_line = parse
   | _	  		{ print (Lexing.lexeme lexbuf) }
 
 and skip_proof = parse
-  | "Save."	{ end_of_line lexbuf }
   | "Save" space
                 { skip_until_point lexbuf }
   | "Qed."  	{ end_of_line lexbuf }
diff --git a/tools/coq-inferior.el b/tools/inferior-coq.el
index b79d97d6..453bd139 100644
--- a/tools/coq-inferior.el
+++ b/tools/inferior-coq.el
@@ -265,7 +265,7 @@ With argument, position cursor at end of buffer."
     (let ((end (point)))
       (beginning-of-line)
       (coq-send-region (point) end)))
-  (next-line 1))
+  (forward-line 1))
 
 (defun coq-send-abort ()
   "Send the command \"Abort.\" to the inferior Coq process."
diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py
new file mode 100755
index 00000000..32c52c7a
--- /dev/null
+++ b/tools/make-both-single-timing-files.py
@@ -0,0 +1,12 @@
+#!/usr/bin/env python
+import sys
+from TimeFileMaker import *
+
+if __name__ == '__main__':
+    USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0]
+    HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table'''
+    sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING)
+    left_dict = get_single_file_times(args[1])
+    right_dict = get_single_file_times(args[2])
+    table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by)
+    print_or_write_table(table, args[3:])
diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py
new file mode 100755
index 00000000..f730a8d6
--- /dev/null
+++ b/tools/make-both-time-files.py
@@ -0,0 +1,16 @@
+#!/usr/bin/env python
+import sys
+from TimeFileMaker import *
+
+if __name__ == '__main__':
+    USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0]
+    HELP_STRING = r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table.
+
+The input is expected to contain lines in the format:
+FILE_NAME (...user: NUMBER_IN_SECONDS...)
+'''
+    sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING)
+    left_dict = get_times(args[1])
+    right_dict = get_times(args[2])
+    table = make_diff_table_string(left_dict, right_dict, sort_by=sort_by)
+    print_or_write_table(table, args[3:])
diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py
new file mode 100755
index 00000000..e66136df
--- /dev/null
+++ b/tools/make-one-time-file.py
@@ -0,0 +1,21 @@
+#!/usr/bin/env python
+import sys
+from TimeFileMaker import *
+
+if __name__ == '__main__':
+    USAGE = 'Usage: %s FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0]
+    HELP_STRING = r'''Formats timing information from the output of `make TIMED=1` into a sorted table.
+
+The input is expected to contain lines in the format:
+FILE_NAME (...user: NUMBER_IN_SECONDS...)
+'''
+    if len(sys.argv) < 2 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]:
+        print(USAGE)
+        if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]:
+            print(HELP_STRING)
+            if len(sys.argv) == 2: sys.exit(0)
+        sys.exit(1)
+    else:
+        times_dict = get_times(sys.argv[1])
+        table = make_table_string(times_dict)
+        print_or_write_table(table, sys.argv[2:])
diff --git a/tools/md5sum.ml b/tools/md5sum.ml
new file mode 100644
index 00000000..2fdcacc8
--- /dev/null
+++ b/tools/md5sum.ml
@@ -0,0 +1,24 @@
+let get_content file =
+  let ic = open_in_bin file in
+  let buf = Buffer.create 2048 in
+  let rec fill () =
+    match input_char ic with
+    | '\r' -> fill () (* NOTE: handles the case on Windows where the
+                         git checkout has included return characters.
+                         See: https://github.com/coq/coq/pull/6305 *)
+    | c -> Buffer.add_char buf c; fill ()
+    | exception End_of_file -> close_in ic; Buffer.contents buf
+  in
+  fill ()
+
+let () =
+  match Sys.argv with
+  | [|_; file|] ->
+      let content = get_content file in
+      let md5 = Digest.to_hex (Digest.string content) in
+      print_string (md5 ^ " " ^ file)
+  | _ ->
+      prerr_endline "Error: This program needs exactly one parameter.";
+      prerr_endline "Usage: ocaml md5sum.ml <FILE>";
+      prerr_endline "Print MD5 (128-bit) checksum of the file content modulo \\r.";
+      exit 1
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index bf82be09..382c39d3 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 {
@@ -11,18 +13,25 @@
 
   let syntax_error lexbuf =
     raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+
+  [@@@ocaml.warning "-3"]       (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
+  let uncapitalize = String.uncapitalize
+
+  let capitalize = String.capitalize
+  [@@@ocaml.warning "+3"]
 }
 
 let space = [' ' '\t' '\n' '\r']
-let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
-let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
-let identchar =
-  ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let lowercase = ['a'-'z']
+let uppercase = ['A'-'Z']
+let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9']
 let caml_up_ident = uppercase identchar*
 let caml_low_ident = lowercase identchar*
 
 rule mllib_list = parse
-  | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
+  | uppercase+ { let s = Lexing.lexeme lexbuf in
+                 s :: mllib_list lexbuf }
+  | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf)
 		in s :: mllib_list lexbuf }
   | "*predef*" { mllib_list lexbuf }
   | space+ { mllib_list lexbuf }
@@ -107,8 +116,18 @@ let error_cannot_parse s (i,j) =
   Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
   exit 1
 
+let same_path_opt s s' =
+  let nf s = (* ./foo/a.ml and foo/a.ml are the same file *)
+    if Filename.is_implicit s
+    then "." // s
+    else s
+  in
+  let s = match s with None -> "." | Some s -> nf s in
+  let s' = match s' with None -> "." | Some s' -> nf s' in
+  s = s'
+
 let warning_ml_clash x s suff s' suff' =
-  if suff = suff' then
+  if suff = suff' && not (same_path_opt s s') then
   eprintf
     "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
     (match s with None -> "." | Some d -> d)
@@ -185,7 +204,7 @@ let mlpack_dependencies () =
   List.iter
     (fun (name,dirname) ->
        let fullname = file_name name dirname in
-       let modname = String.capitalize name in
+       let modname = capitalize name in
        let deps = traite_fichier_modules fullname ".mlpack" in
        let sdeps = String.concat " " deps in
        let efullname = escape fullname in