Imported Upstream version 8.9.0upstream/8.9.0 upstream

author: Benjamin Barenblat <bbaren@debian.org> 2019-02-02 19:29:23 -0500
committer: Benjamin Barenblat <bbaren@debian.org> 2019-02-02 19:29:23 -0500
commit: 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
tree: bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /dev
parent: 9043add656177eeac1491a73d2f3ab92bec0013c (diff)
59 files changed, 2952 insertions, 1732 deletions
diff --git a/dev/README b/dev/README
deleted file mode 100644
index 453f85f0..00000000
--- a/dev/README
+++ /dev/null
@@ -1,50 +0,0 @@
-This directory contains information and tools to help develop the
-                             Coq system
-                       ======================
-
-
-Debugging and profiling (in current directory - see doc/debugging.txt)
------------------------
-
-ocamldebug-coq: to launch ocaml debugger (generated by the configure script)
-
-db:           to install pretty-printers from ocaml debugger
-base_db:      to install raw pretty-printers from ocaml debugger
-
-include:      to install pretty-printers from ocaml toplevel (use with the coq Drop command)
-base_include: to install raw pretty-printers from ocaml toplevel
-
-vm_printers.ml, top_printers.ml: ML pretty-printers for debugging
-
-
-Miscellaneous information about the code (directory doc)
------------------------------------------
-
-changes.md:     (partial) per-version summary of the evolution of Coq ML source
-style.txt:      a few style recommendations for writing Coq ML files
-debugging.md:   help for debugging or profiling
-universes.txt:  help for debugging universes
-translate.txt:  help for using coq translator
-extensions.txt: some help about TACTIC EXTEND
-
-header:         standard header for Coq ML files
-perf-analysis:  analysis of perfs measured on the compilation of user contribs
-cic.dtd:        official dtd of the calc. of ind. constr. for im/ex-portation
-
-
-Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
-----------------------------------------
-"make mli-doc" in coq root directory.
-
-
-Other development tools (directory tools)
------------------------
-
-coqdev.el: helper customizations for everyday Coq development, eg
-  making `compile' work in subdirectories
-
-objects.el: various development utilities at emacs level
-
-anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse
-  location of Anomaly backtraces and jump to them conveniently from
-  the Emacs *compilation* output.
diff --git a/dev/README.md b/dev/README.md
new file mode 100644
index 00000000..4642aaf0
--- /dev/null
+++ b/dev/README.md
@@ -0,0 +1,46 @@
+# This directory contains information and tools to help develop the Coq system
+
+
+## Debugging and profiling (`dev/`)
+**More info on debugging: [`doc/debugging.md`](doc/debugging.md)**
+
+| File | Description |
+| ---- | ----------- |
+| dev/ocamldebug-coq | To launch ocaml debugger (generated by the configure script) |
+| dev/db | To install pretty-printers from ocaml debugger |
+| dev/base_db | To install raw pretty-printers from ocaml debugger |
+| dev/include | To install pretty-printers from ocaml toplevel (use with the coq Drop command) |
+| dev/base_include | To install raw pretty-printers from ocaml toplevel |
+| dev/vm_printers.ml, top_printers.ml | ML pretty-printers for debugging |
+
+
+## Miscellaneous information about the code (`dev/doc`)
+**Beginner's guide to hacking Coq: [`dev/doc/README.md`](doc/README.md)**
+
+| File | Description |
+| ---- | ----------- |
+| [`dev/doc/changes.md`](doc/changes.md) | (partial) Per-version summary of the evolution of Coq ML source |
+| [`dev/doc/style.txt`](doc/style.txt) | A few style recommendations for writing Coq ML files |
+| [`dev/doc/debugging.md`](doc/debugging.md) | Help for debugging or profiling |
+| [`dev/doc/universes.txt`](doc/universes.txt) |  Help for debugging universes |
+| [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND |
+| [`dev/doc/perf-analysis`](doc/perf-analysis)|  Analysis of perfs measured on the compilation of user contribs |
+| [`dev/doc/cic.dtd`](doc/cic.dtd) | Official dtd of the calc. of ind. constr. for im/ex-portation |
+| [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine |
+| [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections |
+| [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine |
+| [`dev/doc/xml-protocol.md`](doc/proof-engine.md) | XML protocol that coqtop and IDEs use to communicate |
+| [`dev/doc/MERGING.md`](doc/MERGING.md) |  How pull requests should be merged into `master` |
+| [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release |
+
+
+## Documentation of ML interfaces using ocamldoc ( `dev/ocamldoc/html`)
+`make mli-doc` in coq root directory.
+
+
+## Other development tools (`dev/tools`)
+
+| File | Description |
+| ---- | ----------- |
+| [`dev/tools/coqdev.el`](tools/coqdev.el) | Helper customizations for everyday Coq development, eg making `compile` work in subdirectories
+| [`dev/tools/objects.el`](tools/objects.el) | Various development utilities at emacs level |
diff --git a/dev/base_include b/dev/base_include
index 1fb80dc0..6f54ecb2 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -15,7 +15,6 @@
 #directory "tactics";;
 #directory "printing";;
 #directory "grammar";;
-#directory "intf";;
 #directory "stm";;
 #directory "vernac";;
 
@@ -109,8 +108,6 @@ open Inductiveops
 open Locusops
 open Find_subterm
 open Unification
-open Miscops
-open Miscops
 open Nativenorm
 open Typeclasses
 open Typeclasses_errors
@@ -190,7 +187,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
+let parse_vernac = Pcoq.parse_string Pvernac.Vernac_.vernac_control;;
 let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
@@ -205,7 +202,9 @@ let e s =
    implicit syntax *)
 
 let constr_of_string s = 
-  Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);;
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Constrintern.interp_constr env sigma (parse_constr s);;
 
 (* get the body of a constant *)
 
@@ -230,9 +229,9 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
+  (fun ?loc _ r -> Nametab.shortest_qualid_of_global ?loc Id.Set.empty r);;
 
-let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
 let _ =
  print_string
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index dc33838f..9b08f517 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -3,26 +3,68 @@
 # Fail on first error
 set -e
 
+# TODO use Docker instead of this
+brew update
+brew unlink python
+brew install opam gnu-time gtk+ expat gtksourceview gdk-pixbuf
+brew unlink python@2
+brew link python3
+pip3 install macpack
+opam init -a -y -j 2 --compiler=ocaml-base-compiler.4.07.1 default https://opam.ocaml.org
+opam switch ocaml-base-compiler.4.07.1
+eval $(opam config env)
+opam update
+opam config list
+opam list
+opam install -j 2 -y camlp5 ocamlfind.1.8.0 num lablgtk.2.18.6 conf-gtksourceview.2
+rm -rf ~/.opam/log/
+opam list
+
 # Configuration setup
 OUTDIR=$PWD/_install
 DMGDIR=$PWD/_dmg
 VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
 APP=bin/CoqIDE_${VERSION}.app
 
+make clean
+./configure -native-compiler no -coqide opt -prefix "$OUTDIR"
+make -j "$NJOBS" byte
+make -j "$NJOBS" world
+make test-suite/misc/universes/all_stdlib.v
+make -j "$NJOBS" world
+make install
+make install-byte
+
 # Create a .app file with CoqIDE, without signing it
-make PRIVATEBINARIES=$APP -j $NJOBS -l2 $APP
+make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP"
 
 # Add Coq to the .app file
-make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
+make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop
+
+if [ -n "$MACOS_CERTIFICATE_IDENTITY" ] && [ -n "$MACOS_CERTIFICATE_PASSWORD" ] && [ -n "$MACOS_CERTIFICATE_BASE_PATH" ]
+then
+    readonly KEYCHAIN=macos-build.keychain
+    # This pile of hacks is required to avoid having to manually validate access to the key through UI
+    security create-keychain -p gitlab "${KEYCHAIN}"
+    security default-keychain -s "${KEYCHAIN}"
+    security unlock-keychain -p gitlab "${KEYCHAIN}"
+    security set-keychain-settings -t 3600 -u "${KEYCHAIN}"
+    security import "${MACOS_CERTIFICATE_BASE_PATH}/foundation.cer" -k ~/Library/Keychains/"${KEYCHAIN}" -T /usr/bin/codesign
+    security import "${MACOS_CERTIFICATE_BASE_PATH}/foundation.p12" -k ~/Library/Keychains/"${KEYCHAIN}" -P "${MACOS_CERTIFICATE_PASSWORD}" -T /usr/bin/codesign
+    security set-key-partition-list -S apple-tool:,apple: -s -k gitlab ~/Library/Keychains/"${KEYCHAIN}"
+    codesign -f -v -s "$MACOS_CERTIFICATE_IDENTITY" "$APP"
+    security default-keychain -s "login.keychain"
+    security delete-keychain "${KEYCHAIN}"
+fi
 
 # Create the dmg bundle
-mkdir -p $DMGDIR
-ln -sf /Applications $DMGDIR/Applications
-cp -r $APP $DMGDIR
+mkdir -p "$DMGDIR"
+ln -sf /Applications "$DMGDIR/Applications"
+cp -r "$APP" "$DMGDIR"
 
 mkdir -p _build
 
 # Temporary countermeasure to hdiutil error 5341
 # head -c9703424 /dev/urandom > $DMGDIR/.padding
 
-hdiutil create -imagekey zlib-level=9 -volname coq-$VERSION-installer-macos -srcfolder $DMGDIR -ov -format UDZO _build/coq-$VERSION-installer-macos.dmg
+hdiutil create -imagekey zlib-level=9 -volname "coq-$VERSION-installer-macos" -srcfolder "$DMGDIR" -ov -format UDZO "_build/coq-$VERSION-installer-macos.dmg"
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 61cf6bc4..8489bcfc 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -1,488 +1,488 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== NOTES ==========
-
-REM For Cygwin setup command line options
-REM see https://cygwin.com/faq/faq.html#faq.setup.cli
-
-REM ========== DEFAULT VALUES FOR PARAMETERS ==========
-
-REM For a description of all parameters, see ReadMe.txt
-
-SET BATCHFILE=%~0
-SET BATCHDIR=%~dp0
-
-REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
-SET ARCH=x86_64
-
-REM see -mode in ReadMe.txt
-SET INSTALLMODE=absolute
-
-REM see -installer in ReadMe.txt
-SET MAKEINSTALLER=N
-
-REM see -ocaml in ReadMe.txt
-SET INSTALLOCAML=N
-
-REM see -make in ReadMe.txt
-SET INSTALLMAKE=N
-
-REM see -destcyg in ReadMe.txt
-SET DESTCYG=C:\bin\cygwin_coq
-
-REM see -destcoq in ReadMe.txt
-SET DESTCOQ=C:\bin\coq
-
-REM see -setup in ReadMe.txt
-SET SETUP=setup-x86_64.exe
-
-REM see -proxy in ReadMe.txt
-IF DEFINED HTTP_PROXY (
-  SET PROXY=%HTTP_PROXY:http://=%
-) else (
-  REM One can't set a variable to empty in DOS, but you can set it to a space this way.
-  REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
-  SET "PROXY= "
-)
-
-REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=http://ftp.inf.tu-dresden.de/software/windows/cygwin32
-
-REM see -cygcache in ReadMe.txt
-SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
-
-REM see -cyglocal in ReadMe.txt
-SET CYGWIN_FROM_CACHE=N
-
-REM see -cygquiet in ReadMe.txt
-SET CYGWIN_QUIET=Y
-
-REM see -srccache in ReadMe.txt
-SET SOURCE_LOCAL_CACHE_WFMT=%BATCHDIR%source_cache
-
-REM see -coqver in ReadMe.txt
-SET COQ_VERSION=8.5pl3
-
-REM see -gtksrc in ReadMe.txt
-SET GTK_FROM_SOURCES=N
-
-REM see -threads in ReadMe.txt
-SET MAKE_THREADS=8
-
-REM see -addon in ReadMe.txt
-SET "COQ_ADDONS= "
-
-REM ========== PARSE COMMAND LINE PARAMETERS ==========
-
-SHIFT
-
-:Parse
-
-IF "%~0" == "-arch" (
-  IF "%~1" == "32" (
-    SET ARCH=i686
-    SET SETUP=setup-x86.exe
-  ) ELSE (
-    IF "%~1" == "64" (
-      SET ARCH=x86_64
-      SET SETUP=setup-x86_64.exe
-    ) ELSE (
-      ECHO "Invalid -arch, valid are 32 and 64"
-      GOTO :EOF
-    )
-  )
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-mode" (
-  IF "%~1" == "mingwincygwin" (
-    SET INSTALLMODE=%~1
-  ) ELSE (
-    IF "%~1" == "absolute" (
-      SET INSTALLMODE=%~1
-    ) ELSE (
-      IF "%~1" == "relocatable" (
-        SET INSTALLMODE=%~1
-      ) ELSE (
-        ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
-        GOTO :EOF
-      )
-    )
-  )
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-installer" (
-  SET MAKEINSTALLER=%~1
-  CALL :CheckYN -installer %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-ocaml" (
-  SET INSTALLOCAML=%~1
-  CALL :CheckYN -installer %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-make" (
-  SET INSTALLMAKE=%~1
-  CALL :CheckYN -installer %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-destcyg" (
-  SET DESTCYG=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-destcoq" (
-  SET DESTCOQ=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-setup" (
-  SET SETUP=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-proxy" (
-  SET PROXY=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-cygrepo" (
-  SET CYGWIN_REPOSITORY=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-cygcache" (
-  SET CYGWIN_LOCAL_CACHE_WFMT=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-cyglocal" (
-  SET CYGWIN_FROM_CACHE=%~1
-  CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-cygquiet" (
-  SET CYGWIN_QUIET=%~1
-  CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-srccache" (
-  SET SOURCE_LOCAL_CACHE_WFMT=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-coqver" (
-  SET COQ_VERSION=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-gtksrc" (
-  SET GTK_FROM_SOURCES=%~1
-  CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-threads" (
-  SET MAKE_THREADS=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-addon" (
-  SET "COQ_ADDONS=%COQ_ADDONS% %~1"
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-
-IF NOT "%~0" == "" (
-  ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
-  ECHO !!! Illegal parameter %~0
-  ECHO Usage:
-  ECHO MakeCoq_MinGW
-  CALL :PrintPars
-  GOTO :EOF
-)
-
-IF NOT EXIST %SETUP% (
-  ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
-  ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option.
-  GOTO :EOF
-)
-
-REM ========== ADJUST PARAMETERS ==========
-
-IF "%INSTALLMODE%" == "mingwincygwin" (
-  SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
-)
-
-IF "%MAKEINSTALLER%" == "Y" (
-  SET INSTALLMODE=relocatable
-)
-
-REM ========== CONFIRM PARAMETERS ==========
-
-CALL :PrintPars
-REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
-IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
-  SET /p ANSWER="Is this correct? y/n "
-  IF NOT "%ANSWER%"=="y" (GOTO :EOF)
-:DontAsk
-
-REM ========== DERIVED VARIABLES ==========
-
-SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
-SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
-SET TARGET_ARCH=%ARCH%-w64-mingw32
-SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
-
-REM Convert pathes to various formats
-REM WFMT = windows format (C:\..)          Used in this batch file.
-REM CFMT = cygwin format (\cygdrive\c\..)  Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
-REM MFMT = MinGW format (C:/...)           Used for the build, because \\ requires escaping. Mingw can handle \ and /.
-
-SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
-SET RESULT_INSTALLDIR_MFMT=%RESULT_INSTALLDIR_WFMT:\=/%
-SET SOURCE_LOCAL_CACHE_MFMT=%SOURCE_LOCAL_CACHE_WFMT:\=/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_MFMT:C:/=/cygdrive/c/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:D:/=/cygdrive/d/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:E:/=/cygdrive/e/%
-
-ECHO CYGWIN INSTALL DIR (WIN)    = %CYGWIN_INSTALLDIR_WFMT%
-ECHO CYGWIN INSTALL DIR (MINGW)  = %CYGWIN_INSTALLDIR_MFMT%
-ECHO CYGWIN INSTALL DIR (CYGWIN) = %CYGWIN_INSTALLDIR_CFMT%
-ECHO RESULT INSTALL DIR (WIN)    = %RESULT_INSTALLDIR_WFMT%
-ECHO RESULT INSTALL DIR (MINGW)  = %RESULT_INSTALLDIR_MFMT%
-ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT%
-
-REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset
-SET MAKE_OPT=-j %MAKE_THREADS%
-
-REM ========== DERIVED CYGWIN SETUP OPTIONS ==========
-
-REM One can't set a variable to empty in DOS, but you can set it to a space this way.
-REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
-SET "CYGWIN_OPT= "
-
-IF "%CYGWIN_FROM_CACHE%" == "Y" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -L
-)
-
-IF "%CYGWIN_QUIET%" == "Y" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
-)
-
-IF "%GTK_FROM_SOURCES%"=="N" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
-)
-
-REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
-REM Otherwise chmod won't work and e.g. the ocaml build will fail.
-REM Cygwin setup does not touch the ACLs of existing folders.
-
-REM Run Cygwin Setup
-
-SET RUNSETUP=Y
-IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
-  SET RUNSETUP=N
-)
-IF NOT "%CYGWIN_QUIET%" == "Y" (
-  SET RUNSETUP=Y
-)
-
-IF "%COQREGTESTING%" == "Y" (
-  ECHO "========== REMOVE EXISTING CYGWIN =========="
-  DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL
-  SET RUNSETUP=Y
-)
-
-SET "EXTRAPACKAGES= "
-
-IF NOT "%APPVEYOR%" == "True" (
-  SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5
-)
-
-ECHO "========== INSTALL CYGWIN =========="
-
-IF "%RUNSETUP%"=="Y" (
-  %SETUP% ^
-    --proxy "%PROXY%" ^
-    --site "%CYGWIN_REPOSITORY%" ^
-    --root "%CYGWIN_INSTALLDIR_WFMT%" ^
-    --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
-    --no-shortcuts ^
-    %CYGWIN_OPT% ^
-    -P make,unzip ^
-    -P gdb,liblzma5 ^
-    -P patch,automake1.14 ^
-    -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
-    -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
-    -P libiconv-devel,libunistring-devel,libncurses-devel ^
-    -P gettext-devel,libgettextpo-devel ^
-    -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
-    -P libfontconfig1 ^
-    -P gtk-update-icon-cache ^
-    -P libtool,automake ^
-    -P intltool ^
-    %EXTRAPACKAGES% ^
-    || GOTO ErrorExit
-
-  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
-  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
-)
-
-IF NOT "%CYGWIN_QUIET%" == "Y" (
-  REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
-  REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
-  :waitsetup
-  tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
-  IF ERRORLEVEL 1 GOTO waitsetup
-)
-
-ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
-
-REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear
-REM HOME (otherwise we get to the home directory of the other installation)
-REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user)
-SET "HOME="
-SET "PROFILEREAD="
-
-copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
-%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
-
-ECHO ========== BUILD COQ ==========
-
-MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
-MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
-
-COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
-COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
-
-%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
-
-ECHO ========== FINISHED ==========
-
-GOTO :EOF
-
-ECHO ========== BATCH FUNCTIONS ==========
-
-:PrintPars
-  REM  01234567890123456789012345678901234567890123456789012345678901234567890123456789
-  ECHO -arch     ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
-  ECHO -mode     ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
-  ECHO           ^<absoloute = install coq in -destcoq absulute path^>
-  ECHO           ^<relocatable = install relocatable coq in -destcoq path^>
-  ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
-  ECHO -ocaml    ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
-  ECHO -make     ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
-  ECHO -destcyg  ^<path to cygwin destination folder^>
-  ECHO -destcoq  ^<path to coq destination folder (mode=absoloute/relocatable)^>
-  ECHO -setup    ^<cygwin setup program name^> (auto adjusted to -arch)
-  ECHO -proxy    ^<internet proxy^>
-  ECHO -cygrepo  ^<cygwin download repository^>
-  ECHO -cygcache ^<local cygwin repository/cache^>
-  ECHO -cyglocal ^<Y or N^> install cygwin from cache
-  ECHO -cygquiet ^<Y or N^> install cygwin without user interaction
-  ECHO -srccache ^<local source code repository/cache^>
-  ECHO -coqver   ^<Coq version to install^>
-  ECHO -gtksrc   ^<Y or N^> build GTK ^(90 min^) or use cygwin version
-  ECHO -threads  ^<1..N^> Number of make threads
-  ECHO -addon    ^<name^>  Enable building selected addon (can be repeated)
-  ECHO(
-  ECHO See ReadMe.txt for a detailed description of all parameters
-  ECHO(
-  ECHO Parameter values (default or currently set):
-  ECHO -arch     = %ARCH%
-  ECHO -mode     = %INSTALLMODE%
-  ECHO -ocaml    = %INSTALLOCAML%
-  ECHO -installer= %MAKEINSTALLER%
-  ECHO -make     = %INSTALLMAKE%
-  ECHO -destcyg  = %DESTCYG%
-  ECHO -destcoq  = %DESTCOQ%
-  ECHO -setup    = %SETUP%
-  ECHO -proxy    = %PROXY%
-  ECHO -cygrepo  = %CYGWIN_REPOSITORY%
-  ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
-  ECHO -cyglocal = %CYGWIN_FROM_CACHE%
-  ECHO -cygquiet = %CYGWIN_QUIET%
-  ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
-  ECHO -coqver   = %COQ_VERSION%
-  ECHO -gtksrc   = %GTK_FROM_SOURCES%
-  ECHO -threads  = %MAKE_THREADS%
-  ECHO -addon    = %COQ_ADDONS%
-  GOTO :EOF
-
-:CheckYN
-  REM Reset errorlevel to 0
-  CMD /c "EXIT /b 0"
-  IF "%2" == "Y" (
-    REM OK Y
-  ) ELSE IF "%2" == "N" (
-    REM OK N
-  ) ELSE (
-    ECHO ERROR Parameter %1 must be Y or N, but is %2
-    GOTO ErrorExit
-  )
-  GOTO :EOF
-
-:ErrorExit
-  ECHO ERROR MakeCoq_MinGW.bat failed
-  EXIT /b 1
+@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== NOTES ==========
+
+REM For Cygwin setup command line options
+REM see https://cygwin.com/faq/faq.html#faq.setup.cli
+
+REM ========== DEFAULT VALUES FOR PARAMETERS ==========
+
+REM For a description of all parameters, see ReadMe.txt
+
+SET BATCHFILE=%~0
+SET BATCHDIR=%~dp0
+
+REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
+SET ARCH=x86_64
+
+REM see -mode in ReadMe.txt
+SET INSTALLMODE=absolute
+
+REM see -installer in ReadMe.txt
+SET MAKEINSTALLER=N
+
+REM see -ocaml in ReadMe.txt
+SET INSTALLOCAML=N
+
+REM see -make in ReadMe.txt
+SET INSTALLMAKE=N
+
+REM see -destcyg in ReadMe.txt
+SET DESTCYG=C:\bin\cygwin_coq
+
+REM see -destcoq in ReadMe.txt
+SET DESTCOQ=C:\bin\coq
+
+REM see -setup in ReadMe.txt
+SET SETUP=setup-x86_64.exe
+
+REM see -proxy in ReadMe.txt
+IF DEFINED HTTP_PROXY (
+  SET PROXY=%HTTP_PROXY:http://=%
+) else (
+  REM One can't set a variable to empty in DOS, but you can set it to a space this way.
+  REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+  SET "PROXY= "
+)
+
+REM see -cygrepo in ReadMe.txt
+SET CYGWIN_REPOSITORY=http://mirror.easyname.at/cygwin
+
+REM see -cygcache in ReadMe.txt
+SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
+
+REM see -cyglocal in ReadMe.txt
+SET CYGWIN_FROM_CACHE=N
+
+REM see -cygquiet in ReadMe.txt
+SET CYGWIN_QUIET=Y
+
+REM see -srccache in ReadMe.txt
+SET SOURCE_LOCAL_CACHE_WFMT=%BATCHDIR%source_cache
+
+REM see -coqver in ReadMe.txt
+SET COQ_VERSION=8.5pl3
+
+REM see -gtksrc in ReadMe.txt
+SET GTK_FROM_SOURCES=N
+
+REM see -threads in ReadMe.txt
+SET MAKE_THREADS=8
+
+REM see -addon in ReadMe.txt
+SET "COQ_ADDONS= "
+
+REM ========== PARSE COMMAND LINE PARAMETERS ==========
+
+SHIFT
+
+:Parse
+
+IF "%~0" == "-arch" (
+  IF "%~1" == "32" (
+    SET ARCH=i686
+    SET SETUP=setup-x86.exe
+  ) ELSE (
+    IF "%~1" == "64" (
+      SET ARCH=x86_64
+      SET SETUP=setup-x86_64.exe
+    ) ELSE (
+      ECHO "Invalid -arch, valid are 32 and 64"
+      GOTO :EOF
+    )
+  )
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-mode" (
+  IF "%~1" == "mingwincygwin" (
+    SET INSTALLMODE=%~1
+  ) ELSE (
+    IF "%~1" == "absolute" (
+      SET INSTALLMODE=%~1
+    ) ELSE (
+      IF "%~1" == "relocatable" (
+        SET INSTALLMODE=%~1
+      ) ELSE (
+        ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
+        GOTO :EOF
+      )
+    )
+  )
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-installer" (
+  SET MAKEINSTALLER=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-ocaml" (
+  SET INSTALLOCAML=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-make" (
+  SET INSTALLMAKE=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-destcyg" (
+  SET DESTCYG=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-destcoq" (
+  SET DESTCOQ=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-setup" (
+  SET SETUP=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-proxy" (
+  SET PROXY=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-cygrepo" (
+  SET CYGWIN_REPOSITORY=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-cygcache" (
+  SET CYGWIN_LOCAL_CACHE_WFMT=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-cyglocal" (
+  SET CYGWIN_FROM_CACHE=%~1
+  CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-cygquiet" (
+  SET CYGWIN_QUIET=%~1
+  CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-srccache" (
+  SET SOURCE_LOCAL_CACHE_WFMT=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-coqver" (
+  SET COQ_VERSION=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-gtksrc" (
+  SET GTK_FROM_SOURCES=%~1
+  CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-threads" (
+  SET MAKE_THREADS=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-addon" (
+  SET "COQ_ADDONS=%COQ_ADDONS% %~1"
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+
+IF NOT "%~0" == "" (
+  ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
+  ECHO !!! Illegal parameter %~0
+  ECHO Usage:
+  ECHO MakeCoq_MinGW
+  CALL :PrintPars
+  GOTO :EOF
+)
+
+IF NOT EXIST %SETUP% (
+  ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
+  ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option.
+  GOTO :EOF
+)
+
+REM ========== ADJUST PARAMETERS ==========
+
+IF "%INSTALLMODE%" == "mingwincygwin" (
+  SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
+)
+
+IF "%MAKEINSTALLER%" == "Y" (
+  SET INSTALLMODE=relocatable
+)
+
+REM ========== CONFIRM PARAMETERS ==========
+
+CALL :PrintPars
+REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
+IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
+  SET /p ANSWER="Is this correct? y/n "
+  IF NOT "%ANSWER%"=="y" (GOTO :EOF)
+:DontAsk
+
+REM ========== DERIVED VARIABLES ==========
+
+SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
+SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
+SET TARGET_ARCH=%ARCH%-w64-mingw32
+SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
+
+REM Convert pathes to various formats
+REM WFMT = windows format (C:\..)          Used in this batch file.
+REM CFMT = cygwin format (\cygdrive\c\..)  Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
+REM MFMT = MinGW format (C:/...)           Used for the build, because \\ requires escaping. Mingw can handle \ and /.
+
+SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
+SET RESULT_INSTALLDIR_MFMT=%RESULT_INSTALLDIR_WFMT:\=/%
+SET SOURCE_LOCAL_CACHE_MFMT=%SOURCE_LOCAL_CACHE_WFMT:\=/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_MFMT:C:/=/cygdrive/c/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:D:/=/cygdrive/d/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:E:/=/cygdrive/e/%
+
+ECHO CYGWIN INSTALL DIR (WIN)    = %CYGWIN_INSTALLDIR_WFMT%
+ECHO CYGWIN INSTALL DIR (MINGW)  = %CYGWIN_INSTALLDIR_MFMT%
+ECHO CYGWIN INSTALL DIR (CYGWIN) = %CYGWIN_INSTALLDIR_CFMT%
+ECHO RESULT INSTALL DIR (WIN)    = %RESULT_INSTALLDIR_WFMT%
+ECHO RESULT INSTALL DIR (MINGW)  = %RESULT_INSTALLDIR_MFMT%
+ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT%
+
+REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset
+SET MAKE_OPT=-j %MAKE_THREADS%
+
+REM ========== DERIVED CYGWIN SETUP OPTIONS ==========
+
+REM One can't set a variable to empty in DOS, but you can set it to a space this way.
+REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+SET "CYGWIN_OPT= "
+
+IF "%CYGWIN_FROM_CACHE%" == "Y" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -L
+)
+
+IF "%CYGWIN_QUIET%" == "Y" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
+)
+
+IF "%GTK_FROM_SOURCES%"=="N" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+)
+
+REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
+REM Otherwise chmod won't work and e.g. the ocaml build will fail.
+REM Cygwin setup does not touch the ACLs of existing folders.
+
+REM Run Cygwin Setup
+
+SET RUNSETUP=Y
+IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
+  SET RUNSETUP=N
+)
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+  SET RUNSETUP=Y
+)
+
+IF "%COQREGTESTING%" == "Y" (
+  ECHO "========== REMOVE EXISTING CYGWIN =========="
+  DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL
+  SET RUNSETUP=Y
+)
+
+SET "EXTRAPACKAGES= "
+
+IF NOT "%APPVEYOR%" == "True" (
+  SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5
+)
+
+ECHO "========== INSTALL CYGWIN =========="
+
+IF "%RUNSETUP%"=="Y" (
+  %SETUP% ^
+    --proxy "%PROXY%" ^
+    --site "%CYGWIN_REPOSITORY%" ^
+    --root "%CYGWIN_INSTALLDIR_WFMT%" ^
+    --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
+    --no-shortcuts ^
+    %CYGWIN_OPT% ^
+    -P make,unzip ^
+    -P gdb,liblzma5 ^
+    -P patch,automake1.14 ^
+    -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
+    -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+    -P libiconv-devel,libunistring-devel,libncurses-devel ^
+    -P gettext-devel,libgettextpo-devel ^
+    -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
+    -P libfontconfig1 ^
+    -P gtk-update-icon-cache ^
+    -P libtool,automake ^
+    -P intltool ^
+    %EXTRAPACKAGES% ^
+    || GOTO ErrorExit
+
+  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
+)
+
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+  REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
+  REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
+  :waitsetup
+  tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
+  IF ERRORLEVEL 1 GOTO waitsetup
+)
+
+ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
+
+REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear
+REM HOME (otherwise we get to the home directory of the other installation)
+REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user)
+SET "HOME="
+SET "PROFILEREAD="
+
+copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
+
+ECHO ========== BUILD COQ ==========
+
+MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
+
+COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
+COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
+
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
+
+ECHO ========== FINISHED ==========
+
+GOTO :EOF
+
+ECHO ========== BATCH FUNCTIONS ==========
+
+:PrintPars
+  REM  01234567890123456789012345678901234567890123456789012345678901234567890123456789
+  ECHO -arch     ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
+  ECHO -mode     ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
+  ECHO           ^<absoloute = install coq in -destcoq absulute path^>
+  ECHO           ^<relocatable = install relocatable coq in -destcoq path^>
+  ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
+  ECHO -ocaml    ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
+  ECHO -make     ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
+  ECHO -destcyg  ^<path to cygwin destination folder^>
+  ECHO -destcoq  ^<path to coq destination folder (mode=absoloute/relocatable)^>
+  ECHO -setup    ^<cygwin setup program name^> (auto adjusted to -arch)
+  ECHO -proxy    ^<internet proxy^>
+  ECHO -cygrepo  ^<cygwin download repository^>
+  ECHO -cygcache ^<local cygwin repository/cache^>
+  ECHO -cyglocal ^<Y or N^> install cygwin from cache
+  ECHO -cygquiet ^<Y or N^> install cygwin without user interaction
+  ECHO -srccache ^<local source code repository/cache^>
+  ECHO -coqver   ^<Coq version to install^>
+  ECHO -gtksrc   ^<Y or N^> build GTK ^(90 min^) or use cygwin version
+  ECHO -threads  ^<1..N^> Number of make threads
+  ECHO -addon    ^<name^>  Enable building selected addon (can be repeated)
+  ECHO(
+  ECHO See ReadMe.txt for a detailed description of all parameters
+  ECHO(
+  ECHO Parameter values (default or currently set):
+  ECHO -arch     = %ARCH%
+  ECHO -mode     = %INSTALLMODE%
+  ECHO -ocaml    = %INSTALLOCAML%
+  ECHO -installer= %MAKEINSTALLER%
+  ECHO -make     = %INSTALLMAKE%
+  ECHO -destcyg  = %DESTCYG%
+  ECHO -destcoq  = %DESTCOQ%
+  ECHO -setup    = %SETUP%
+  ECHO -proxy    = %PROXY%
+  ECHO -cygrepo  = %CYGWIN_REPOSITORY%
+  ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
+  ECHO -cyglocal = %CYGWIN_FROM_CACHE%
+  ECHO -cygquiet = %CYGWIN_QUIET%
+  ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
+  ECHO -coqver   = %COQ_VERSION%
+  ECHO -gtksrc   = %GTK_FROM_SOURCES%
+  ECHO -threads  = %MAKE_THREADS%
+  ECHO -addon    = %COQ_ADDONS%
+  GOTO :EOF
+
+:CheckYN
+  REM Reset errorlevel to 0
+  CMD /c "EXIT /b 0"
+  IF "%2" == "Y" (
+    REM OK Y
+  ) ELSE IF "%2" == "N" (
+    REM OK N
+  ) ELSE (
+    ECHO ERROR Parameter %1 must be Y or N, but is %2
+    GOTO ErrorExit
+  )
+  GOTO :EOF
+
+:ErrorExit
+  ECHO ERROR MakeCoq_MinGW.bat failed
+  EXIT /b 1
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 16c972e8..7e606b55 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -14,30 +14,30 @@
 rcfile=~/.bash_profile
 donefile=~/.bash_profile.upated
 
+# to learn about `exec >> $file`, see https://www.tldp.org/LDP/abs/html/x17974.html
+exec >> $rcfile
+
 if [ ! -f $donefile ] ; then
 
-    echo >> $rcfile
-    
-    if [ "$1" != "" -a "$1" != " " ]; then
-      echo export http_proxy="http://$1" >> $rcfile
-      echo export https_proxy="http://$1" >> $rcfile
-      echo export ftp_proxy="http://$1" >> $rcfile
+    if [ "$1" != "" ] && [ "$1" != " " ]; then
+      echo export http_proxy="http://$1"
+      echo export https_proxy="http://$1"
+      echo export ftp_proxy="http://$1"
     fi
-    
-    mkdir -p $RESULT_INSTALLDIR_CFMT/bin
+
+    mkdir -p "$RESULT_INSTALLDIR_CFMT/bin"
 
     # A tightly controlled path helps to avoid issues
     # Note: the order is important: first have the cygwin binaries, then the mingw binaries in the path!
     # Note: /bin is mounted at /usr/bin and /lib at /usr/lib and it is common to use /usr/bin in PATH
     # See cat /proc/mounts
-    echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows" >> $rcfile
+    echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows"
 
     # find and xargs complain if the environment is larger than (I think) 8k.
     # ORIGINAL_PATH (set by cygwin) can be a few k and exceed the limit
-    echo unset ORIGINAL_PATH >> $rcfile
-    
+    echo unset ORIGINAL_PATH
     # Other installations of OCaml will mess up things
-    echo unset OCAMLLIB >> $rcfile
+    echo unset OCAMLLIB
 
     touch $donefile
 fi
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
index cbcf14ec..3bba451e 100644
--- a/dev/build/windows/difftar-folder.sh
+++ b/dev/build/windows/difftar-folder.sh
@@ -42,7 +42,7 @@ fi
 if [ "$strip" -gt 0 ] ; then
   # Get the path/name of the first file from teh tar and extract the first $strip path components
   # This assumes that the first file in the tar file has at least $strip many path components
-  prefix=$(tar -t -f $tarfile | head -1 | cut -d / -f -$strip)/
+  prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/
 else
   prefix=
 fi
@@ -60,13 +60,13 @@ mkdir -p "$empty"
 
 # Print information (this is ignored by patch)
 
-echo diff/patch file created on $(date) with:
-echo difftar-folder.sh $@
-echo TARFILE=    $tarfile
-echo FOLDER=     $folder
-echo TARSTRIP=   $strip
-echo TARPREFIX=  $prefix
-echo ORIGFOLDER= $orig
+echo diff/patch file created on "$(date)" with:
+echo difftar-folder.sh "$@"
+echo TARFILE=    "$tarfile"
+echo FOLDER=     "$folder"
+echo TARSTRIP=   "$strip"
+echo TARPREFIX=  "$prefix"
+echo ORIGFOLDER= "$orig"
 
 # Make sure tar uses english output (for Mod time differs)
 export LC_ALL=C
@@ -76,14 +76,14 @@ tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod tim
   # Substitute ': Mod time differs' with nothing
   file=${file/: Mod time differs/}
   # Check if file exists
-  if [ -f "$folder/$file" ] ; then 
+  if [ -f "$folder/$file" ] ; then
     # Extract original file
     tar -x -a -f "$tarfile" --strip $strip --directory "$orig" "$prefix$file"
     # Compute diff
-    diff -u "$orig/$file" "$folder/$file" 
+    diff -u "$orig/$file" "$folder/$file"
   fi
 done
 
 if [ -d "$new" ] ; then
-  diff -u -r --unidirectional-new-file $empty $new
+  diff -u -r --unidirectional-new-file "$empty" "$new"
 fi
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 86cc5f2d..070af6b4 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -159,19 +159,19 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
   # Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
   log1() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1.log"  2>"$LOGS/$LOGTARGET-$1.err"
+    "$@" >"$LOGS/$LOGTARGET-$1_log.txt"  2>"$LOGS/$LOGTARGET-$1_err.txt"
   }
 
   # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
   log2() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1-$2.log" 2>"$LOGS/$LOGTARGET-$1-$2.err"
+    "$@" >"$LOGS/$LOGTARGET-$1-$2_log.txt" 2>"$LOGS/$LOGTARGET-$1-$2_err.txt"
   }
 
   # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
   log_1_3() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1-$3.log" 2>"$LOGS/$LOGTARGET-$1-$3.err"
+    "$@" >"$LOGS/$LOGTARGET-$1-$3_log.txt" 2>"$LOGS/$LOGTARGET-$1-$3_err.txt"
   }
 
   # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -179,26 +179,26 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
     { local -; set +x; } 2> /dev/null
     LOGTARGETEX=$1
     shift
-    "$@" >"$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2>"$LOGS/$LOGTARGET-$LOGTARGETEX.err"
+    "$@" >"$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" 2>"$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt"
   }
 else
   # If COQREGTESTING, log to log files and console
   # Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
   log1() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1.log" | sed -e "s/^/$LOGTARGET-$1.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1.err" | sed -e "s/^/$LOGTARGET-$1.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1_log.txt" | sed -e "s/^/$LOGTARGET-$1_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1_err.txt" | sed -e "s/^/$LOGTARGET-$1_err.txt: /" 1>&2)
   }
 
   # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
   log2() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2.log" | sed -e "s/^/$LOGTARGET-$1-$2.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2.err" | sed -e "s/^/$LOGTARGET-$1-$2.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2_log.txt" | sed -e "s/^/$LOGTARGET-$1-$2_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2_err.txt" | sed -e "s/^/$LOGTARGET-$1-$2_err.txt: /" 1>&2)
   }
 
   # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
   log_1_3() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3.log" | sed -e "s/^/$LOGTARGET-$1-$3.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3.err" | sed -e "s/^/$LOGTARGET-$1-$3.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3_log.txt" | sed -e "s/^/$LOGTARGET-$1-$3_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3_err.txt" | sed -e "s/^/$LOGTARGET-$1-$3_err.txt: /" 1>&2)
   }
 
   # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -206,7 +206,7 @@ else
     { local -; set +x; } 2> /dev/null
     LOGTARGETEX=$1
     shift
-    "$@" > >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.log" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.log: /") 2> >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.err" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_err.txt: /" 1>&2)
   }
 fi
 
@@ -238,9 +238,10 @@ fi
 # $1 file server name including protocol prefix
 # $2 file name (without extension)
 # $3 file extension
-# $4 number of path levels to strip from tar (usually 1)
-# $5 module name (if different from archive)
-# $6 expand folder name (if different from module name)
+# $4 [optional] number of path levels to strip from tar (usually 1)
+# $5 [optional] module name (if different from archive)
+# $6 [optional] expand folder name (if different from module name)
+# $7 [optional] module base name (used as 2nd choice for patches, defaults to $5)
 # ------------------------------------------------------------------------------
 
 function get_expand_source_tar {
@@ -263,6 +264,12 @@ function get_expand_source_tar {
     folder=$name
   fi
 
+  if [ "$#" -ge 7 ] ; then
+    basename=$7
+  else
+    basename=$name
+  fi
+
   # Set logging target
   logtargetold=$LOGTARGET
   LOGTARGET=$name
@@ -314,8 +321,11 @@ function get_expand_source_tar {
   fi
 
   # Patch if patch file exists
+  # First try specific patch file name then generic patch file name
   if [ -f "$PATCHES/$name.patch" ] ; then
     log1 patch -p1 -i "$PATCHES/$name.patch"
+  elif  [ -f "$PATCHES/$basename.patch" ] ; then
+    log1 patch -p1 -i "$PATCHES/$basename.patch"
   fi
 
   # Go back to base folder
@@ -340,6 +350,7 @@ function get_expand_source_tar {
 # $3 file extension
 # $4 [optional] number of path levels to strip from tar (usually 1)
 # $5 [optional] module name (if different from archive)
+# $6 [optional] module base name (used as 2nd choice for patches, defaults to $5)
 # ------------------------------------------------------------------------------
 
 function build_prep {
@@ -356,6 +367,12 @@ function build_prep {
     name=$2
   fi
 
+  if [ "$#" -ge 6 ] ; then
+    basename=$6
+  else
+    basename=$name
+  fi
+
   # Set installer section to not set by default
   installersection=
 
@@ -368,7 +385,7 @@ function build_prep {
 
     touch "$FLAGFILES/$name.started"
 
-    get_expand_source_tar "$1" "$2" "$3" "$strip" "$name"
+    get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" "$name" "$basename"
 
     cd "$name"
 
@@ -409,7 +426,7 @@ function build_prep_overlay {
       # $1_CI_REF must have been a tag or hash, not a branch
       ver="$ref"
   fi
-  build_prep "$url" "$ver" tar.gz 1 "$1-$ver"
+  build_prep "$url" "$ver" tar.gz 1 "$1-$ver" "$1"
 }
 
 # ------------------------------------------------------------------------------
@@ -666,6 +683,17 @@ function installer_addon_end {
   fi
 }
 
+# ------------------------------------------------------------------------------
+# Set all timeouts in all .v files to 1000
+# Since timeouts can lead to CI failures, this is useful
+#
+# parameters: none
+# ------------------------------------------------------------------------------
+
+function coq_set_timeouts_1000 {
+  find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/g'
+}
+
 ###################### MODULE BUILD FUNCTIONS #####################
 
 ##### SED #####
@@ -1343,11 +1371,10 @@ function copy_coq_license {
     install -D doc/LICENSE                    "$PREFIXCOQ/license_readme/coq/LicenseDoc.txt"
     install -D LICENSE                        "$PREFIXCOQ/license_readme/coq/License.txt"
     install -D plugins/micromega/LICENSE.sos  "$PREFIXCOQ/license_readme/coq/LicenseMicromega.txt"
-    install -D README                         "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true
-    install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true
-    install -D README.win                     "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true
-    install -D README.doc                     "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true
-    install -D CHANGES                        "$PREFIXCOQ/license_readme/coq/Changes.txt"
+    # FIXME: this is not the micromega license
+    # It only applies to code that was copied into one single file!
+    install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
+    install -D CHANGES.md                     "$PREFIXCOQ/license_readme/coq/Changes.md"
     install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
@@ -1620,7 +1647,7 @@ function make_addon_equations {
   installer_addon_dependency equations
   if build_prep_overlay Equations; then
     installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" ""
-    # Note: PATH is autmatically saved/restored by build_prep / build_post
+    # Note: PATH is automatically saved/restored by build_prep / build_post
     PATH=$COQBIN:$PATH
     logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
     log1 make
@@ -1668,7 +1695,7 @@ function make_addon_ssreflect {
 function make_addon_ltac2 {
   installer_addon_dependency ltac2
   if build_prep_overlay ltac2; then
-    installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactics language" ""
+    installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" ""
     log1 make all
     log2 make install
     build_post
@@ -1680,6 +1707,7 @@ function make_addon_ltac2 {
 function make_addon_unicoq {
   installer_addon_dependency unicoq
   if build_prep_overlay unicoq; then
+    installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" ""
     log1 coq_makefile -f Make -o Makefile
     log1 make
     log2 make install
@@ -1694,6 +1722,7 @@ function make_addon_mtac2 {
   make_addon_unicoq
   installer_addon_dependency_end
   if build_prep_overlay mtac2; then
+    installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." ""
     log1 coq_makefile -f _CoqProject -o Makefile
     log1 make
     log2 make install
@@ -1778,8 +1807,8 @@ function install_addon_vst {
     install_glob "progs" '*.v' "$VSTDEST/progs/"
     install_glob "progs" '*.c' "$VSTDEST/progs/"
     install_glob "progs" '*.h' "$VSTDEST/progs/"
-    install_glob "veric" '*.v' "$VSTDEST/msl/"
-    install_glob "veric" '*.vo' "$VSTDEST/msl/"
+    install_glob "veric" '*.v' "$VSTDEST/veric/"
+    install_glob "veric" '*.vo' "$VSTDEST/veric/"
 
     # Install VST documentation files
     install_glob "." 'LICENSE' "$VSTDEST"
@@ -1792,11 +1821,20 @@ function install_addon_vst {
     install_glob "." '_CoqProject-export' "$VSTDEST/progs"
 }
 
+function vst_patch_compcert_refs {
+  find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \
+    -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \
+    -e 's/From compcert Require/From VST.compcert Require/g'
+}
+
 function make_addon_vst {
   installer_addon_dependency vst
   if build_prep_overlay VST; then
     installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off"
-    log1 make IGNORECOQVERSION=true $MAKE_OPT
+    # log1 coq_set_timeouts_1000
+    log1 vst_patch_compcert_refs
+    # The usage of the shell variable ARCH in VST collides with the usage in this shellscript
+    logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT
     log1 install_addon_vst
     build_post
   fi
diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch
new file mode 100755
index 00000000..2c8c4637
--- /dev/null
+++ b/dev/build/windows/patches_coq/VST.patch
@@ -0,0 +1,15 @@
+diff --git a/Makefile b/Makefile
+index 4a119042..fdfac13e 100755
+--- a/Makefile
++++ b/Makefile
+@@ -76,8 +76,8 @@ endif
+
+ COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND)
+
+-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d))
+-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d))
++COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d))
++EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d))
+
+ # for SSReflect
+ ifdef MATHCOMP
diff --git a/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch b/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch
deleted file mode 100644
index d9b134b2..00000000
--- a/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch
+++ /dev/null
@@ -1,21 +0,0 @@
---- aac-tactics-v8.8.orig\Tutorial.v	2018-05-30 16:09:06.000000000 +0200
-+++ aac-tactics-v8.8\Tutorial.v	2018-08-24 19:47:25.000000000 +0200
-@@ -9,16 +9,14 @@
- (** * Tutorial for using the [aac_tactics] library.
- 
-    Depending on your installation, either modify the following two
-    lines, or add them to your .coqrc files, replacing "."  with the
-    path to the [aac_tactics] library. *)
- 
--Add Rec LoadPath "." as AAC_tactics.
--Add ML Path ".".
--Require Import AAC.
--Require Instances.
-+Require Import AAC_tactics.AAC.
-+Require AAC_tactics.Instances.
- Require Arith ZArith.
- 
- (** ** Introductory example 
- 
-    Here is a first example with relative numbers ([Z]): one can
-    rewrite an universally quantified hypothesis modulo the
diff --git a/dev/build/windows/patches_coq/quickchick-v1.0.2.patch b/dev/build/windows/patches_coq/quickchick.patch
index d03749ba..1afa6e7f 100644..100755
--- a/dev/build/windows/patches_coq/quickchick-v1.0.2.patch
+++ b/dev/build/windows/patches_coq/quickchick.patch
@@ -24,15 +24,3 @@ ORIGFOLDER= quickchick-v1.0.2.orig
 +	$(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick"
  #	 $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick
  #	 $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick
- 
---- quickchick-v1.0.2.orig/src/Show.v	2018-08-22 18:21:39.000000000 +0200
-+++ quickchick-v1.0.2/src/Show.v	2018-08-27 09:21:35.893961900 +0200
-@@ -228,7 +228,7 @@
-       match s with 
-         | EmptyString => (if b then ")" else "", b)
-         | String a s => 
--          let (s', b) := aux s (orb b (nat_of_ascii a =? 32)) in
-+          let (s', b) := aux s (orb b (nat_of_ascii a =? 32)%nat) in
-           (String a s', b)
-       end in
-   let (s', b) := aux s false in
diff --git a/dev/checker.dbg b/dev/checker.dbg
new file mode 100644
index 00000000..b2323b61
--- /dev/null
+++ b/dev/checker.dbg
@@ -0,0 +1,6 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer clib.cma
+load_printer dynlink.cma
+load_printer lib.cma
+load_printer check.cma
diff --git a/dev/checker_db b/dev/checker_db
new file mode 100644
index 00000000..327e636c
--- /dev/null
+++ b/dev/checker_db
@@ -0,0 +1,39 @@
+source checker.dbg
+
+load_printer checker_printers.cmo
+
+install_printer Checker_printers.pP
+
+install_printer Checker_printers.ppfuture
+
+install_printer Checker_printers.ppid
+install_printer Checker_printers.pplab
+install_printer Checker_printers.ppmbid
+install_printer Checker_printers.ppdir
+install_printer Checker_printers.ppmp
+install_printer Checker_printers.ppcon
+install_printer Checker_printers.ppproj
+install_printer Checker_printers.ppkn
+install_printer Checker_printers.ppmind
+install_printer Checker_printers.ppind
+
+install_printer Checker_printers.ppbigint
+
+install_printer Checker_printers.ppintset
+install_printer Checker_printers.ppidset
+
+install_printer Checker_printers.ppidmapgen
+
+install_printer Checker_printers.ppididmap
+
+install_printer Checker_printers.ppuni
+install_printer Checker_printers.ppuni_level
+install_printer Checker_printers.ppuniverse_set
+install_printer Checker_printers.ppuniverse_instance
+install_printer Checker_printers.ppauniverse_context
+install_printer Checker_printers.ppuniverse_context
+install_printer Checker_printers.ppconstraints
+install_printer Checker_printers.ppuniverse_context_future
+install_printer Checker_printers.ppuniverses
+
+install_printer Checker_printers.pploc
diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml
new file mode 100644
index 00000000..40ae1a7b
--- /dev/null
+++ b/dev/checker_printers.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open Names
+open Univ
+
+let pp   x = Pp.pp_with Format.std_formatter x
+
+(** Future printer *)
+
+let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
+
+(* name printers *)
+let ppid id = pp (Id.print id)
+let pplab l = pp (Label.print l)
+let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
+let ppdir dir = pp (DirPath.print dir)
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
+let ppcon con = pp(Constant.debug_print con)
+let ppproj con = pp(Constant.debug_print (Projection.constant con))
+let ppkn kn = pp(str (KerName.to_string kn))
+let ppmind kn = pp(MutInd.debug_print kn)
+let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
+
+(* term printers *)
+let ppbigint n = pp (str (Bigint.to_string n));;
+
+let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
+let ppintset l = pp (prset int (Int.Set.elements l))
+let ppidset l = pp (prset Id.print (Id.Set.elements l))
+
+let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
+
+let pridmap pr l =
+  let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in
+  prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
+let ppidmap pr l = pp (pridmap pr l)
+
+let pridmapgen l =
+  let dom = Id.Set.elements (Id.Map.domain l) in
+  if dom = [] then str "[]" else
+  str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]"
+let ppidmapgen l = pp (pridmapgen l)
+
+let prididmap = pridmap (fun _ -> Id.print)
+let ppididmap = ppidmap (fun _ -> Id.print)
+
+let pP s = pp (hov 0 s)
+
+(* proof printers *)
+let ppuni u = pp(Universe.pr u)
+let ppuni_level u = pp (Level.pr u)
+
+let ppuniverse_set l = pp (LSet.pr l)
+let ppuniverse_instance l = pp (Instance.pr l)
+let ppauniverse_context l = pp (AUContext.pr Level.pr l)
+let ppuniverse_context l = pp (pr_universe_context Level.pr l)
+let ppconstraints c = pp (pr_constraints Level.pr c)
+let ppuniverse_context_future c =
+  let ctx = Future.force c in
+    ppuniverse_context ctx
+let ppuniverses u = pp (Univ.pr_universes u)
+
+let pploc x = let (l,r) = Loc.unloc x in
+  print_string"(";print_int l;print_string",";print_int r;print_string")"
diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli
new file mode 100644
index 00000000..2f9500c5
--- /dev/null
+++ b/dev/checker_printers.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Printers for the ocaml toplevel. *)
+
+val pp : Pp.t -> unit
+val pP : Pp.t -> unit (* with surrounding box *)
+
+val ppfuture : 'a Future.computation -> unit
+
+val ppid : Names.Id.t -> unit
+val pplab : Names.Label.t -> unit
+val ppmbid : Names.MBId.t -> unit
+val ppdir : Names.DirPath.t -> unit
+val ppmp : Names.ModPath.t -> unit
+val ppcon : Names.Constant.t -> unit
+val ppproj : Names.Projection.t -> unit
+val ppkn : Names.KerName.t -> unit
+val ppmind : Names.MutInd.t -> unit
+val ppind : Names.inductive -> unit
+
+val ppbigint : Bigint.bigint -> unit
+
+val ppintset : Int.Set.t -> unit
+val ppidset : Names.Id.Set.t -> unit
+
+val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t
+val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit
+
+val pridmapgen : 'a Names.Id.Map.t -> Pp.t
+val ppidmapgen : 'a Names.Id.Map.t -> unit
+
+val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t
+val ppididmap : Names.Id.t Names.Id.Map.t -> unit
+
+(* Universes *)
+val ppuni : Univ.Universe.t -> unit
+val ppuni_level : Univ.Level.t -> unit (* raw *)
+val ppuniverse_set : Univ.LSet.t -> unit
+val ppuniverse_instance : Univ.Instance.t -> unit
+val ppauniverse_context : Univ.AUContext.t -> unit
+val ppuniverse_context : Univ.UContext.t -> unit
+val ppconstraints : Univ.Constraint.t -> unit
+val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
+val ppuniverses : Univ.universes -> unit
+
+val pploc : Loc.t -> unit
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 43d680af..60a86362 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project:
    developer who merges the PR on Coq. There are plans to improve this, cf.
    [#6724](https://github.com/coq/coq/issues/6724).
 
-Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
 
 Advanced GitLab CI information
 ------------------------------
@@ -136,15 +136,35 @@ rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci`
 and `make install` is run, then the `_install_ci` directory
 persists to and is used by the next jobs.
 
-Artifacts can also be downloaded from the GitLab repository.
-Currently, available artifacts are:
-- the Coq executables and stdlib, in three copies varying in
-  architecture and OCaml version used to build Coq.
-- the Coq documentation, built only in the `build:base` job. When submitting
-  a documentation PR, this can help reviewers checking the rendered result.
+### Artifacts
 
-As an exception to the above, jobs testing that compilation triggers
-no OCaml warnings build Coq in parallel with other tests.
+Build artifacts from GitLab can be linked / downloaded in a systematic
+way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts)
+for more information. For example, to access the documentation of the
+`master` branch, you can do:
+
+https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
+
+Browsing artifacts is also possible:
+https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
+
+Above, you can replace `master` and `job` by the desired GitLab branch and job name.
+
+Currently available artifacts are:
+
+- the Coq executables and stdlib, in four copies varying in
+  architecture and OCaml version used to build Coq:
+  https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
+
+- the Coq documentation, built in the `doc:*` jobs. When submitting
+  a documentation PR, this can help reviewers checking the rendered result:
+
+  + Coq's Reference Manual [master branch]
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
+  + Coq's Standard Library Documentation [master branch]
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base
+  + Coq's ML API Documentation [master branch]
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api
 
 ### GitLab and Windows
 
@@ -152,6 +172,11 @@ If your repository has access to runners tagged `windows`, setting the
 secret variable `WINDOWS` to `enabled` will add jobs building Windows
 versions of Coq (32bit and 64bit).
 
+If the secret variable `WINDOWS` is set to `enabled_all_addons`,
+an extended set of addons will be added to the Windows installer.
+This leads to a considerable runtime in CI so this is not enabled
+by default for pipelines for pull requests.
+
 The Windows jobs are enabled on Coq's repository, where pipelines for
 pull requests run.
 
@@ -171,6 +196,6 @@ but if you wish to save more time you can skip the job by setting
 
 This means you will need to change its value when the Docker image
 needs to be updated. You can do so for a single pipeline by starting
-it through the web interface..
+it through the web interface.
 
 See also [`docker/README.md`](docker/README.md).
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 8f53877f..d2176e32 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -10,6 +10,6 @@ bash opam64/install.sh
 
 opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH
 eval "$(opam config env)"
-opam install -y num ocamlfind camlp5
+opam install -y num ocamlfind camlp5 ounit
 
 cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 13367794..dd5555e4 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -9,7 +9,8 @@
 ########################################################################
 # MathComp
 ########################################################################
-: "${mathcomp_CI_REF:=mathcomp-1.7.0}"
+# Latest commit on master as of Sep 27, 2018
+: "${mathcomp_CI_REF:=5f8d45b54aa98732ec3de43d91814459d5a2f2e4}"
 : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}"
 : "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}"
 
@@ -20,79 +21,95 @@
 ########################################################################
 # UniMath
 ########################################################################
-: "${UniMath_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${UniMath_CI_REF:=17a5f224feb42b562ded5fec79ea937dcb45764c}"
 : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}"
 : "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}"
 
 ########################################################################
 # Unicoq + Mtac2
 ########################################################################
-: "${unicoq_CI_REF:=v1.3-8.8}"
+# Latest commit on master as of Sep 27, 2018
+: "${unicoq_CI_REF:=1cec038ab34e03109f5587a8aecda1f6c53495dd}"
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
 : "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
 
-: "${mtac2_CI_REF:=v1.0.1-coq8.8}"
+# Latest commit on master-sync as of Sep 27, 2018
+: "${mtac2_CI_REF:=e65c2560e5098df5e7333f19db97e9f39e46c3ee}"
 : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}"
 : "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}"
 
 ########################################################################
 # Mathclasses + Corn
 ########################################################################
-: "${math_classes_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${math_classes_CI_REF:=0f530c713db886ab692bba49862a1cbcbebc8610}"
 : "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}"
 : "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}"
 
-: "${Corn_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${Corn_CI_REF:=f505e489829a968074f53fe18b70a292ad94a9d0}"
 : "${Corn_CI_GITURL:=https://github.com/coq-community/corn}"
 : "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}"
 
 ########################################################################
 # Iris
 ########################################################################
-: "${stdpp_CI_REF:=master}"
+# std++ commit pinned in Iris
+: "${stdpp_CI_REF:=4fb641edc8d74fbba01fed33d9acbc8a423ea601}"
 : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}"
 : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
 
-: "${Iris_CI_REF:=master}"
+# Iris commit pinned in LambdaRust
+: "${Iris_CI_REF:=85425d47be677d05d74caff5e1a8a85289d96ae1}"
 : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}"
 : "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
 
-: "${lambdaRust_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${lambdaRust_CI_REF:=fd46e6625eef509a80896dccf6c976545b17ab90}"
 : "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}"
 : "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}"
 
 ########################################################################
 # HoTT
 ########################################################################
-: "${HoTT_CI_REF:=V8.8}"
+# Latest commit on master as of Sep 3, 2018
+: "${HoTT_CI_REF:=333face272e39175a1b342e14c86c316f572f51f}"
 : "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}"
 : "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}"
 
 ########################################################################
 # Ltac2
 ########################################################################
-: "${ltac2_CI_REF:=0.1}"
+: "${ltac2_CI_REF:=v8.9}"
 : "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}"
 : "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}"
 
 ########################################################################
 # GeoCoq
 ########################################################################
-: "${GeoCoq_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${GeoCoq_CI_REF:=a13b48840898fec207b382ab42c0bf0b2f62024b}"
 : "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}"
 : "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}"
 
 ########################################################################
 # Flocq
 ########################################################################
-: "${Flocq_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${Flocq_CI_REF:=ff6fc12f269ca055b7b6fd88247ac2697ff6e687}"
 : "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}"
 : "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}"
 
 ########################################################################
 # Coquelicot
 ########################################################################
-# ATTENTION: The archive URL might depend on the version
+# The URL for downloading a tgz snapshot of the master branch is
+# https://scm.gforge.inria.fr/anonscm/gitweb?p=coquelicot/coquelicot.git;a=snapshot;h=refs/heads/master;sf=tgz
+# See https://gforge.inria.fr/scm/browser.php?group_id=3599
+# Since this URL doesn't fit to our standard mechanism and since Coquelicot doesn't seem to change frequently,
+# we use a fixed version, which has a download path which does fit to our standard mechanism.
+# ATTENTION: The archive URL might depend on the version!
 : "${Coquelicot_CI_REF:=coquelicot-3.0.2}"
 : "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
 : "${Coquelicot_CI_ARCHIVEURL:=https://gforge.inria.fr/frs/download.php/file/37523}"
@@ -100,53 +117,64 @@
 ########################################################################
 # CompCert
 ########################################################################
-# Note: The latest release version of CompCert (3.3) does not compile with Coq 8.8.1
-# This is caused by a compatibility issue with OCaml 4.0.7
-: "${CompCert_CI_REF:=17f9d839df12511a7e327f2840855e70af5ede47}"
+# Latest commit on master as of Sep 27, 2018
+: "${CompCert_CI_REF:=020be062488d755236f296fff760c7491e11997b}"
 : "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}"
 : "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}"
 
 ########################################################################
 # VST
 ########################################################################
-# Note: The latest release version of VST (2.2) does not compile with Coq 8.8.1
-# Note: newer versions of VST have issues with buildability and licensing
-: "${VST_CI_REF:=e49605cf1f1e5ae3bbec3d6554122427a94ae986}"
+# Latest commit on master as of Dec 10, 2018
+: "${VST_CI_REF:=f6afb456db69df66c366c36b2d0218d92813f546}"
 : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}"
 : "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}"
 
 ########################################################################
+# cross-crypto
+########################################################################
+# Latest commit on master as of Sep 27, 2018
+: "${cross_crypto_CI_REF:=453da7e0541798f36d82b6c67a3f4461cd5dc773}"
+: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}"
+: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}"
+
+########################################################################
 # fiat_parsers
 ########################################################################
-: "${fiat_parsers_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${fiat_parsers_CI_REF:=a41e7ee1c5152aecedb354a112d5c8121a499d30}"
 : "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}"
 : "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}"
 
 ########################################################################
 # fiat_crypto
 ########################################################################
-: "${fiat_crypto_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${fiat_crypto_CI_REF:=059f186db67852ac17de78dab1987aab77dd4bdb}"
 : "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}"
 : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}"
 
 ########################################################################
 # formal-topology
 ########################################################################
-: "${formal_topology_CI_REF:=ci}"
+# Latest commit on ci as of Sep 27, 2018
+: "${formal_topology_CI_REF:=a2f1aa04db253e4f90fb2aae724cfca42ccd53ab}"
 : "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}"
 : "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}"
 
 ########################################################################
 # coq-dpdgraph
 ########################################################################
-: "${coq_dpdgraph_CI_REF:=coq-v8.8}"
+# Latest commit on coq-master as of Sep 27, 2018
+: "${coq_dpdgraph_CI_REF:=e14e2bc0108a593f7c64d9af3fc4aec9e8fb1397}"
 : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}"
 : "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}"
 
 ########################################################################
 # CoLoR
 ########################################################################
-: "${CoLoR_CI_REF:=master}"
+# Latest commit on master as of Nov 5, 2018
+: "${CoLoR_CI_REF:=4ce3a9fb5f58501aef3c0727c8ba8cc38917399d}"
 : "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}"
 : "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}"
 
@@ -160,77 +188,101 @@
 ########################################################################
 # TLC
 ########################################################################
-: "${tlc_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${tlc_CI_REF:=6bce3c31e5c74d9f953de3620deadd9f4cc04023}"
 : "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}"
 
 ########################################################################
 # Bignums
 ########################################################################
-: "${bignums_CI_REF:=V8.8.0}"
+# Latest commit on master as of Sep 27, 2018
+: "${bignums_CI_REF:=f1a63cb4cce9a79e4406275fbb0ee2269947f8d2}"
 : "${bignums_CI_GITURL:=https://github.com/coq/bignums}"
 : "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}"
 
 ########################################################################
 # bedrock2
 ########################################################################
-: "${bedrock2_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${bedrock2_CI_REF:=cbf50671ba2d9235060d4e4747d0860f127f3995}"
 : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}"
 : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}"
 
 ########################################################################
 # Equations
 ########################################################################
-: "${Equations_CI_REF:=v1.1-8.8}"
+# Latest commit on master as of Sep 26, 2018
+: "${Equations_CI_REF:=477cb9d8aac85e03dad3f992f99646e14d803a0c}"
 : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}"
 : "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}"
 
 ########################################################################
 # Elpi
 ########################################################################
-: "${Elpi_CI_REF:=coq-v8.8}"
+: "${Elpi_CI_REF:=coq-v8.9}"
 : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}"
 : "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}"
 
 ########################################################################
 # fcsl-pcm
 ########################################################################
-: "${fcsl_pcm_CI_REF:=master}"
+# Latest commit on master as of Sep 27, 2018
+: "${fcsl_pcm_CI_REF:=51ade0a882ae2ac7df071b41d468df1813504c81}"
 : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}"
 : "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}"
 
 ########################################################################
+# pidetop
+########################################################################
+# Latest commit on v8.9 as of Sep 27, 2018
+: "${pidetop_CI_REF:=ef42320bc0ab75f313e9476e8c8c945ae2116cb5}"
+: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}"
+: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}"
+
+########################################################################
 # ext-lib
 ########################################################################
-# Note: This is the latest commit of the v8.8 branch as of August 31st 2018
-: "${ext_lib_CI_REF:=5dd9cfa51f96fcb785c7c31d8c6bf55af5d93f27}"
+# Latest commit on master as of Sep 27, 2018
+: "${ext_lib_CI_REF:=a9c138921fb8c2601e64f1a1702a689120d456f3}"
 : "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}"
 : "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}"
 
 ########################################################################
 # simple-io
 ########################################################################
-: "${simple_io_CI_REF:=0.2}"
+# Latest commit on master as of Sep 27, 2018
+: "${simple_io_CI_REF:=e627c087ed8225d70aa7aafe882448fea31fef32}"
 : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}"
 : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}"
 
 ########################################################################
 # quickchick
 ########################################################################
-: "${quickchick_CI_REF:=v1.0.2}"
+# Latest commit on master as of Sep 27, 2018
+: "${quickchick_CI_REF:=fae47245b75f049c462601d88e4df2e063841a3b}"
 : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}"
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
 
 ########################################################################
+# plugin_tutorial
+########################################################################
+# Latest commit on master as of Sep 27, 2018
+: "${plugin_tutorial_CI_REF:=b303b75c18734accc9cd7efe82307b0424426e3f}"
+: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
+: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
+
+########################################################################
 # menhirlib
 ########################################################################
-: "${menhirlib_CI_REF:=20180827}"
+# Latest commit on master as of Sep 27, 2018
+: "${menhirlib_CI_REF:=9e4b304bdbcc1f8d433e005a46eb10480e7ae880}"
 : "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/coq-menhirlib}"
 : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}"
 
 ########################################################################
 # aac-tactics
 ########################################################################
-# Note: this is the latest commit of the v8.8 branch as of August 31st 2018
-: "${aactactis_CI_REF:=86ac28259030649ef51460e4de2441c8a1017751}"
+# Latest commit on v8.9 as of Dec 17, 2018
+: "${aactactis_CI_REF:=c469b26e409b1bde6a64546df85226079796dbe7}"
 : "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
 : "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 6fc4293d..7af648f0 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -93,7 +93,7 @@ make()
 # this installs just the ssreflect library of math-comp
 install_ssreflect()
 {
-  echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
+  echo 'Installing ssreflect'
 
   git_download mathcomp
 
@@ -102,14 +102,12 @@ install_ssreflect()
     make -f Makefile.coq ssreflect/all_ssreflect.vo && \
     make -f Makefile.coq install )
 
-  echo -en 'travis_fold:end:ssr.install\\r'
-
 }
 
 # this installs just the ssreflect + algebra library of math-comp
 install_ssralg()
 {
-  echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r'
+  echo 'Installing ssralg'
 
   git_download mathcomp
 
@@ -118,6 +116,4 @@ install_ssralg()
     make -f Makefile.coq algebra/all_algebra.vo && \
     make -f Makefile.coq install )
 
-  echo -en 'travis_fold:end:ssralg.install\\r'
-
 }
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh
new file mode 100755
index 00000000..900d12c1
--- /dev/null
+++ b/dev/ci/ci-cross-crypto.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+FORCE_GIT=1
+git_download cross_crypto
+
+( cd "${CI_BUILD_DIR}/cross_crypto" && git submodule update --init --recursive && make )
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
index 7f4ef77d..9b4a06fd 100755
--- a/dev/ci/ci-elpi.sh
+++ b/dev/ci/ci-elpi.sh
@@ -3,7 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-FORCE_GIT=1
 git_download Elpi
 
 ( cd "${CI_BUILD_DIR}/Elpi" && make && make install )
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index e0395754..6bf31383 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -10,4 +10,5 @@ fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-d
 fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
+  ./etc/ci/remove_autogenerated.sh && \
   make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 9a0726a1..7eeeb093 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download HoTT
 
-( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make )
+( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index 6960a8b9..bc49193b 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -9,13 +9,15 @@ install_ssreflect
 git_download lambdaRust
 
 # Extract required version of Iris
-Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
+# Iris is already pinned in ci-basic-overlays.sh
+#Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup Iris
 git_download Iris
 
 # Extract required version of std++
-stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
+# std++ is already pinned in ci-basic-overlays.sh
+#stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup std++
 git_download stdpp
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 74f1a627..a74f9fa4 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -1,5 +1,6 @@
 #!/usr/bin/env bash
 
+# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
new file mode 100755
index 00000000..d22b9c8f
--- /dev/null
+++ b/dev/ci/ci-pidetop.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download pidetop
+
+# Travis / Gitlab have different filesystem layout due to use of
+# `-local`. We need to improve this divergence but if we use Dune this
+# "local" oddity goes away automatically so not bothering...
+if [ -d "$COQBIN/../lib/coq" ]; then
+   COQLIB="$COQBIN/../lib/coq/"
+else
+   COQLIB="$COQBIN/../"
+fi
+
+( cd "${CI_BUILD_DIR}/pidetop" && jbuilder build @install )
+
+echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 58bbb722..60436e67 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -8,11 +8,6 @@ wget -qO- "${sf_lf_CI_TARURL}"  | tar xvz
 wget -qO- "${sf_plf_CI_TARURL}" | tar xvz
 wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz
 
-sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
-sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
-
-( cd lf && make clean && make )
-
-( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
-
+( cd lf  && make clean && make )
+( cd plf && make clean && make )
 ( cd vfa && make clean && make )
diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple-io.sh
index ddc1590d..e7bcd80d 100755
--- a/dev/ci/ci-simple-io.sh
+++ b/dev/ci/ci-simple-io.sh
@@ -1,7 +1,6 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-
 . "${ci_dir}/ci-common.sh"
 
 git_download simple_io
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
new file mode 100644
index 00000000..919e2a73
--- /dev/null
+++ b/dev/ci/docker/README.md
@@ -0,0 +1,36 @@
+## Overall Docker Setup for Coq's CI.
+
+This directory provides Docker images to be used by Coq's CI. The
+images do support Docker autobuild on `hub.docker.com` and Gitlab's
+private registry.
+
+Gitlab CI will build and tag a Docker by default for every job if the
+`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this
+variable is usually set to `false` indeed to avoid booting a useless
+job.
+
+## Manual Building
+
+You can also manually build and push any image:
+
+- Build the image `docker build -t base:$VERSION .`
+
+To upload/push to your hub:
+
+- Create a https://hub.docker.com account.
+- Login into your space `docker login --username=$USER`
+- Push the image:
+  + `docker tag base:$VERSION $USER/base:$VERSION`
+  + `docker push $USER/base:$VERSION`
+
+## Debugging / Misc
+
+To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>`
+
+Each `RUN` command creates an "layer", thus a Docker build is
+incremental and it always help to put things updated more often at the
+end.
+
+## Possible Improvements:
+
+- Use ARG for customizing versions, centralize variable setup;
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index da12f122..332597f3 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-v8.8-V2018-09-20"
+# CACHEKEY: "bionic_coq-v8.9-V2018-10-22"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -8,52 +8,63 @@ ENV DEBIAN_FRONTEND="noninteractive"
 
 RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of the image, the test-suite and external projects
-        m4 automake autoconf time wget rsync git gcc-multilib opam \
+        m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \
         # Dependencies of lablgtk (for CoqIDE)
         libgtk2.0-dev libgtksourceview2.0-dev \
-        texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk xindy texlive-science tipa hevea \
-        python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \
-        python3-setuptools python3-wheel python3-pip
+        # Dependencies of stdlib and sphinx doc
+        texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
+        xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
+        python3-sphinx python3-sphinx-rtd-theme python3-sphinxcontrib.bibtex \
+        # Dependencies of source-doc and coq-makefile
+        texlive-science tipa
 
+# More dependencies of the sphinx doc
 RUN pip3 install antlr4-python3-runtime
 
+# We need to install OPAM 2.0 manually for now.
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+
 # Basic OPAM setup
 ENV NJOBS="2" \
+    OPAMJOBS="2" \
     OPAMROOT=/root/.opamcache \
-    OPAMROOTISOK="true"
+    OPAMROOTISOK="true" \
+    OPAMYES="true"
 
 # Base opam is the set of base packages required by Coq
 ENV COMPILER="4.02.3"
 
-RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update
-
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0" \
-    CI_OPAM="menhir.20180530 ppx_tools_versioned.5.2 ppx_deriving.4.1.5 ocaml-migrate-parsetree.1.0.11 ocamlgraph.1.8.8"
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.1.1 ounit.2.0.8" \
+    CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV CAMLP5_VER="6.14" \
     COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
-RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM && \
-    opam install -j $NJOBS camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
+# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3
+RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
+    opam install ocamlfind.1.8.0 && \
+    opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
 
 # base+32bit switch
-RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER
+RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
+    opam install ocamlfind.1.8.0 && \
+    opam install $BASE_OPAM camlp5.$CAMLP5_VER
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.0" \
     CAMLP5_VER_EDGE="7.06" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2"
 
-RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
+RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \
+    opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
+
+# EDGE+flambda switch, we install CI_OPAM as to be able to use
+# `ci-template-flambda` with everything.
+RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \
+    opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
 
-# BE+flambda switch
-RUN opam switch -y -j $NJOBS "${COMPILER_EDGE}+flambda" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM && \
-    opam install -j $NJOBS camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
+RUN opam clean -a -c
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index ee1b17b6..66f964a3 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -1,131 +1,132 @@
-@ECHO OFF
-
-REM This script builds and signs the Windows packages on Gitlab
-
-ECHO "Start Time"
-TIME /T
-
-REM List currently used cygwin and target folders for debugging / maintenance purposes
-
-ECHO "Currently used cygwin folders"
-DIR C:\cygwin*
-ECHO "Currently used target folders"
-DIR C:\coq*
-
-if %ARCH% == 32 (
-  SET ARCHLONG=i686
-  SET CYGROOT=C:\cygwin
-  SET SETUP=setup-x86.exe
-)
-
-if %ARCH% == 64 (
-  SET ARCHLONG=x86_64
-  SET CYGROOT=C:\cygwin64
-  SET SETUP=setup-x86_64.exe
-)
-
-SET DESTCOQ=C:\coq%ARCH%_inst
-
-CALL :MakeUniqueFolder %CYGROOT% CYGROOT
-CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
-
-powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CYGCACHE=%CYGROOT%\var\cache\setup
-SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
-SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
-SET COQREGTESTING=Y
-SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
-
-if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
-if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
-
-call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-  -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
-  -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-  -addon=bignums ^
-  -addon=equations ^
-  -addon=ltac2 ^
-  -addon=mtac2 ^
-  -addon=mathcomp ^
-  -addon=menhir ^
-  -addon=menhirlib ^
-  -addon=compcert ^
-  -addon=vst ^
-  -addon=aactactics ^
-  -addon=extlib ^
-  -addon=quickchick ^
-  -addon=coquelicot ^
-  -make=N ^
-  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
-
-ECHO "Start Artifact Creation"
-TIME /T
-
-mkdir artifacts
-
-CALL :CopyLogFiles
-
-copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
-REM The open source archive is only required for release builds
-IF DEFINED WIN_CERTIFICATE_PATH (
-  7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
-) ELSE (
-  REM In non release builds, create a dummy file
-  ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
-)
-
-REM DO NOT echo the signing command below, as this would leak secrets in the logs
-IF DEFINED WIN_CERTIFICATE_PATH (
-  IF DEFINED WIN_CERTIFICATE_PASSWORD (
-    ECHO Signing package
-    @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
-    signtool verify /pa dev\nsis\*.exe
-  )
-)
-
-ECHO "Finished Artifact Creation"
-TIME /T
-
-CALL :CleanupFolders
-
-ECHO "Finished Cleanup"
-TIME /T
-
-GOTO :EOF
-
-:CopyLogFiles
-  ECHO Copy log files for artifact upload
-  MKDIR artifacts\buildlogs
-  COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
-  MKDIR artifacts\filelists
-  COPY %CYGROOT%\build\filelists\* artifacts\filelists
-  MKDIR artifacts\flagfiles
-  COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
-  GOTO :EOF
-
-:CleanupFolders
-  ECHO "Cleaning %CYGROOT%"
-  DEL /S /F /Q "%CYGROOT%" > NUL
-  ECHO "Cleaning %DESTCOQ%"
-  DEL /S /F /Q "%DESTCOQ%" > NUL
-  GOTO :EOF
-
-:MakeUniqueFolder
-  REM Create a uniquely named folder
-  REM This script is safe because folder creation is atomic - either we create it or fail
-  REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
-  REM %2 = name of the variable which receives the unique folder name
-  SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
-  MKDIR "%UNIQUENAME%"
-  IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
-  SET "%2=%UNIQUENAME%"
-  GOTO :EOF
-
-:ErrorCopyLogFilesAndExit
-  CALL :CopyLogFiles
-  REM fall through
-
-:ErrorExit
-  CALL :CleanupFolders
-  ECHO ERROR %0 failed
-  EXIT /b 1
+@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+ECHO "Start Time"
+TIME /T
+
+REM List currently used cygwin and target folders for debugging / maintenance purposes
+
+ECHO "Currently used cygwin folders"
+DIR C:\ci\cygwin*
+ECHO "Currently used target folders"
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
+
+if %ARCH% == 32 (
+  SET ARCHLONG=i686
+  SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+  SET ARCHLONG=x86_64
+  SET SETUP=setup-x86_64.exe
+)
+
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
+
+powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
+SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
+SET COQREGTESTING=Y
+SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
+
+if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
+if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+
+call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+  -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
+  -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+  -addon=bignums ^
+  -addon=equations ^
+  -addon=ltac2 ^
+  -addon=mtac2 ^
+  -addon=mathcomp ^
+  -addon=menhir ^
+  -addon=menhirlib ^
+  -addon=compcert ^
+  -addon=extlib ^
+  -addon=quickchick ^
+  -addon=coquelicot ^
+  -addon=vst ^
+  -addon=aactactics ^
+  -make=N ^
+  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+mkdir artifacts
+
+CALL :CopyLogFiles
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
+REM The open source archive is only required for release builds
+IF DEFINED WIN_CERTIFICATE_PATH (
+  7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+) ELSE (
+  REM In non release builds, create a dummy file
+  ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
+)
+
+REM DO NOT echo the signing command below, as this would leak secrets in the logs
+IF DEFINED WIN_CERTIFICATE_PATH (
+  IF DEFINED WIN_CERTIFICATE_PASSWORD (
+    ECHO Signing package
+    @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
+    signtool verify /pa dev\nsis\*.exe
+  )
+)
+
+ECHO "Finished Artifact Creation"
+TIME /T
+
+CALL :CleanupFolders
+
+ECHO "Finished Cleanup"
+TIME /T
+
+GOTO :EOF
+
+:CopyLogFiles
+  ECHO Copy log files for artifact upload
+  MKDIR artifacts\buildlogs
+  COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
+  MKDIR artifacts\filelists
+  COPY %CYGROOT%\build\filelists\* artifacts\filelists
+  MKDIR artifacts\flagfiles
+  COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
+  GOTO :EOF
+
+:CleanupFolders
+  ECHO "Cleaning %CYGROOT%"
+  RMDIR /S /Q "%CYGROOT%"
+  ECHO "Cleaning %DESTCOQ%"
+  RMDIR /S /Q "%DESTCOQ%"
+  GOTO :EOF
+
+:MakeUniqueFolder
+  REM Create a uniquely named folder
+  REM This script is safe because folder creation is atomic - either we create it or fail
+  REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
+  REM %2 = name of the variable which receives the unique folder name
+  SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
+  MKDIR "%UNIQUENAME%"
+  IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
+  SET "%2=%UNIQUENAME%"
+  GOTO :EOF
+
+:ErrorCopyLogFilesAndExit
+  CALL :CopyLogFiles
+  REM fall through
+
+:ErrorExit
+  CALL :CleanupFolders
+  ECHO ERROR %0 failed
+  EXIT /b 1
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
index be0058b6..d812df3e 100644
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -1,3 +1,5 @@
+#!/bin/sh
+
 if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_REF=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp
diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh
new file mode 100644
index 00000000..575df074
--- /dev/null
+++ b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh
@@ -0,0 +1,8 @@
+_OVERLAY_BRANCH=pure-sharing-flag
+
+if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index b8628979..68afe7ee 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,6 +1,8 @@
 # Add overlays for your pull requests in this directory
 
-An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+When your pull request breaks an external project we test in our CI and you
+have prepared a branch with the fix, you can add an "overlay" to your pull
+request to test it with the adapted version of the external project.
 
 An overlay is a file which defines where to look for the patched version so that
 testing is possible. It redefines some variables from
@@ -22,10 +24,12 @@ and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
 ```
+#!/bin/sh
+
 if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_REF=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp
 fi
 ```
 
-(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh))
+(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh))
diff --git a/dev/core.dbg b/dev/core.dbg
index 57c13690..972ba701 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -2,8 +2,8 @@ source camlp5.dbg
 load_printer threads.cma
 load_printer str.cma
 load_printer clib.cma
-load_printer lib.cma
 load_printer dynlink.cma
+load_printer lib.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
@@ -16,5 +16,4 @@ load_printer tactics.cma
 load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
-load_printer intf.cma
 load_printer ltac_plugin.cmo
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
new file mode 100644
index 00000000..000f21c2
--- /dev/null
+++ b/dev/doc/MERGING.md
@@ -0,0 +1,136 @@
+# Merging changes in Coq
+
+This document describes how patches, submitted as pull requests (PRs) on the
+`master` branch, should be merged into the main repository
+(https://github.com/coq/coq).
+
+## Code owners
+
+The [CODEOWNERS](../../.github/CODEOWNERS) file describes, for each part of the
+system, two owners. One is the principal maintainer of the component, the other
+is the secondary maintainer.
+
+When a PR is submitted, GitHub will automatically ask the principal
+maintainer for a review. If the PR touches several parts, all the
+corresponding principal maintainers will be asked for a review.
+
+Maintainers are never assigned as reviewer on their own PRs.
+
+If a principal maintainer submits a PR that changes the component they own, they
+must assign the secondary maintainer as reviewer. They should also do it if they
+know they are not available to do the review.
+
+## Reviewing
+
+When maintainers receive a review request, they are expected to:
+
+* Put their name in the assignee field, if they are in charge of the component
+  that is the main target of the patch (or if they are the only maintainer asked
+  to review the PR).
+* Review the PR, approve it or request changes.
+* If they are the assignee, check if all reviewers approved the PR. If not,
+  regularly ping the author (if changes should be implemented) or the reviewers
+  (if reviews are missing). The assignee ensures that any requests for more
+  discussion have been granted. When the discussion has converged and ALL
+  REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
+  process described below.
+
+In all cases, maintainers can delegate reviews to the other maintainer of the
+same component, except if it would lead to a maintainer reviewing their own
+patch.
+
+A maintainer is expected to be reasonably reactive, but no specific timeframe is
+given for reviewing.
+
+(*) In case a component is touched in a trivial way (adding/removing one file in
+a `Makefile`, etc), or by applying a systematic refactoring process (global
+renaming for instance) that has been reviewed globally, the assignee can
+say in a comment they think a review is not required and proceed with the merge.
+
+### Breaking changes
+
+If the PR breaks compatibility of some external projects in CI, then fixes to
+those external projects should have been prepared (cf. the relevant sub-section
+in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
+with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
+
+Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
+
+If overlays are missing, ask the author to prepare them and label the PR with
+the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
+
+When fixes are ready, there are two cases to consider:
+
+- For patches that are backward compatible (best scenario), you should get the
+  external project maintainers to integrate them before merging the PR.
+- For patches that are not backward compatible (which is often the case when
+  patching plugins after an update to the Coq API), you can proceed to merge
+  the PR and then notify the external project maintainers they can merge the
+  patch.
+
+## Merging
+
+Once all reviewers approved the PR, the assignee is expected to check that CI
+completed without relevant failures, and that the PR comes with appropriate
+documentation and test cases. If not, they should leave a comment on the PR and
+put the approriate label. Otherwise, they are expected to merge the PR using the
+[merge script](../tools/merge-pr.sh).
+
+When CI has a few failures which look spurious, restarting the corresponding
+jobs is a good way of ensuring this was indeed the case.
+To restart a job on Travis, you should connect using your GitHub account;
+being part of the Coq organization on GitHub should give you the permission
+to do so.
+To restart a job on GitLab CI, you should sign into GitLab (this can be done
+using a GitHub account); if you are part of the
+[Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry"
+button; otherwise, send a request to join the organization.
+
+When the PR has conflicts, the assignee can either:
+- ask the author to rebase the branch, fixing the conflicts
+- warn the author that they are going to rebase the branch, and push to the
+  branch directly
+
+In both cases, CI should be run again.
+
+In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix
+the conflicts in the merge commit (following the same steps as below), and push
+to `master` directly. Don't use the GitHub interface to fix these conflicts.
+
+To merge the PR proceed in the following way
+```
+$ git checkout master
+$ git pull
+$ dev/tools/merge-pr.sh XXXX
+$ git push upstream
+```
+where `XXXX` is the number of the PR to be merged and `upstream` is the name
+of your remote pointing to `git@github.com:coq/coq.git`.
+Note that you are only supposed to merge PRs into `master`. PRs should rarely
+target the stable branch, but when it is the case they are the responsibility
+of the release manager.
+
+This script conducts various checks before proceeding to merge. Don't bypass them
+without a good reason to, and in that case, write a comment in the PR thread to
+explain the reason.
+
+Maintainers MUST NOT merge their own patches.
+
+DON'T USE the GitHub interface for merging, since it will prevent the automated
+backport script from operating properly, generates bad commit messages, and a
+messy history when there are conflicts.
+
+### Merge script dependencies
+
+The merge script passes option `-S` to `git merge` to ensure merge commits
+are signed. Consequently, it depends on the GnuPG command utility being
+installed and a GPG key being available. Here is a short documentation on
+how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/.
+
+The script depends on a few other utilities. If you are a Nix user, the
+simplest way of getting them is to run `nix-shell` first.
+
+**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG
+is not out of the box. Installing explicitly "pinentry-mac" seems important for
+typing of passphrase to work correctly (see also this
+[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)).
diff --git a/dev/doc/README.md b/dev/doc/README.md
new file mode 100644
index 00000000..223cf628
--- /dev/null
+++ b/dev/doc/README.md
@@ -0,0 +1,77 @@
+# Beginner's guide to hacking Coq
+
+## Getting dependencies
+
+Assuming one is running Ubuntu (if not, replace `apt` with the package manager of choice)
+
+```
+$ sudo apt-get install make opam git
+
+# At the time of writing, <latest-ocaml-version> is 4.07.0.
+# The latest version number is available at: https://ocaml.org/releases/
+
+$ opam init --comp <latest-ocaml-version>
+
+# Then follow the advice displayed at the end as how to update your
+  ~/.bashrc and ~/.ocamlinit files.
+
+$ source ~/.bashrc
+$ opam install camlp5
+
+# needed if you want to build "coqide" target
+
+$ sudo apt-get install liblablgtksourceview2-ocaml-dev \
+  libgtk2.0-dev libgtksourceview2.0-dev
+$ opam install lablgtk
+```
+
+## Building `coqtop`
+The general workflow is to first setup a development environment with
+the correct `configure` settings, then hacking on Coq, make-ing, and testing.
+
+
+This document will use `$JOBS` to refer to the number of parallel jobs one
+is willing to have with `make`.
+
+
+```
+$ git clone git clone https://github.com/coq/coq.git
+$ cd coq
+$ ./configure -profile devel
+$ make -j $JOBS # Make once for `merlin`(autocompletion tool)
+
+<hack>
+
+$ make -j $JOBS states # builds just enough to run coqtop
+$ bin/coqtop -compile <test_file_name.v>
+<goto hack until stuff works>
+
+<run test-suite>
+```
+
+To learn how to run the test suite, you can read
+[`test-suite/README.md`](../../test-suite/README.md).
+
+## Coq functions of interest
+- `Coqtop.start`: This function is the main entry point of coqtop.
+- `Coqtop.parse_args `: This function is responsible for parsing command-line arguments.
+- `Coqloop.loop`: This function implements the read-eval-print loop.
+- `Vernacentries.interp`: This function is called to execute the Vernacular command user have typed.
+                       It dispatches the control to specific functions handling different Vernacular command.
+- `Vernacentries.vernac_check_may_eval`: This function handles the `Check ...` command.
+
+
+## Development environment + tooling
+- [`Merlin`](https://github.com/ocaml/merlin) for autocomplete.
+- [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup)
+
+## A note about rlwrap
+
+When using `rlwrap coqtop` make sure the version of `rlwrap` is at least
+`0.42`, otherwise you will get
+
+```
+rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory
+```
+
+If this happens either update or use an alternate readline wrapper like `ledit`.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ab78b095..ca73cd63 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,205 @@
+## Changes between Coq 8.8 and Coq 8.9
+
+### ML API
+
+Names
+
+- In `Libnames`, the type `reference` and its two constructors `Qualid` and
+  `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity,
+  `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be
+  replaced by a test using `qualid_is_ident`. Extracting the `ident` part of a
+  `qualid` can be done using `qualid_basename`.
+
+Misctypes
+
+- Syntax for universe sorts and kinds has been moved from `Misctypes`
+  to `Glob_term`, as these are turned into kernel terms by
+  `Pretyping`.
+
+Proof engine
+
+- More functions have been changed to use `EConstr`, notably the
+  functions in `Evd`, and in particular `Evd.define`.
+
+  Note that the core function `EConstr.to_constr` now _enforces_ by
+  default that the resulting term is ground, that is to say, free of
+  Evars. This is usually what you want, as open terms should be of
+  type `EConstr.t` to benefit from the invariants the `EConstr` API is
+  meant to guarantee.
+
+  In case you'd like to violate this API invariant, you can use the
+  `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note
+  that setting this flag to false is deprecated so it is only meant to
+  be used as to help port pre-EConstr code.
+
+- A few type alias have been deprecated, in all cases the message
+  should indicate what the canonical form is. An important change is
+  the move of `Globnames.global_reference` to `Names.GlobRef.t`.
+
+- Unification API returns `evar_map option` instead of `bool * evar_map`
+  with the guarantee that the `evar_map` was unchanged if the boolean
+  was false.
+
+ML Libraries used by Coq
+
+- Introduction of a `Smart` module for collecting `smart*` functions, e.g.
+  `Array.Smart.map`.
+- Uniformization of some names, e.g. `Array.Smart.fold_left_map` instead
+  of `Array.smartfoldmap`.
+
+Printer.ml API
+
+- The mechanism in `Printer` that allowed dynamically overriding `pr_subgoals`,
+  `pr_subgoal` and `pr_goal` was removed to simplify the code.  It was
+  earlier used by PCoq.
+
+Kernel
+
+- The following renamings happened:
+  - `Context.Rel.t` into `Constr.rel_context`
+  - `Context.Named.t` into `Constr.named_context`
+  - `Context.Compacted.t` into `Constr.compacted_context`
+  - `Context.Rel.Declaration.t` into `Constr.rel_declaration`
+  - `Context.Named.Declaration.t` into `Constr.named_declaration`
+  - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration`
+
+Source code organization
+
+- We have eliminated / fused some redundant modules and relocated a
+  few interfaces files. The `intf` folder is gone, and now for example
+  `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and
+  so on. Changes should be compatible, but in a few cases stricter
+  layering requirements may mean that functions have moved. In all
+  cases adapting is a matter of changing the module name.
+
+Vernacular commands
+
+- The implementation of vernacular commands has been refactored so it
+  is self-contained now, including the parsing and extension
+  mechanisms. This involves a couple of non-backward compatible
+  changes due to layering issues, where some functions have been moved
+  from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in
+  `tactics/`. In all cases adapting is a matter of changing the module
+  name.
+
+Primitive number parsers
+
+- For better modularity, the primitive parsers for `positive`, `N` and `Z`
+  have been split over three files (`plugins/syntax/positive_syntax.ml`,
+  `plugins/syntax/n_syntax.ml`, `plugins/syntax/z_syntax.ml`).
+
+Parsing
+
+- Manual uses of the `Pcoq.Gram` module have been deprecated. Wrapper modules
+  `Pcoq.Entry` and `Pcoq.Parsable` were introduced to replace it.
+
+Termops
+
+- Internal printing functions have been placed under the
+  `Termops.Internal` namespace.
+
+### Unit testing
+
+The test suite now allows writing unit tests against OCaml code in the Coq
+code base. Those unit tests create a dependency on the OUnit test framework.
+
+### Transitioning away from Camlp5
+
+In an effort to reduce dependency on camlp5, the use of several grammar macros
+is discouraged. Coq is now shipped with its own preprocessor, called coqpp,
+which serves the same purpose as camlp5.
+
+To perform the transition to coqpp macros, one first needs to change the
+extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are
+handled yet.
+
+Due to parsing constraints, the syntax of the macros is slightly different, but
+updating the source code is mostly a matter of straightforward
+search-and-replace. The main differences are summarized below.
+
+#### OCaml code
+
+Every piece of toplevel OCaml code needs to be wrapped into braces.
+
+For instance, code of the form
+```
+let myval = 0
+```
+should be turned into
+```
+{
+let myval = 0
+}
+```
+
+#### TACTIC EXTEND
+
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions with braces
+- if not there yet, add a leading `|` to the first rule
+
+For instance, code of the form:
+```
+TACTIC EXTEND my_tac
+  [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ]
+| [ "tac2" tactic(t) ] -> [ mytac2 t ]
+END
+```
+should be turned into
+```
+TACTIC EXTEND my_tac
+| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t }
+| [ "tac2" tactic(t) ] -> { mytac2 t }
+END
+```
+
+#### VERNAC EXTEND
+
+Not handled yet.
+
+#### ARGUMENT EXTEND
+
+Not handled yet.
+
+#### GEXTEND
+
+Most plugin writers do not need this low-level interface, but for the sake of
+completeness we document it.
+
+Steps to perform are:
+- replace `GEXTEND` with `GRAMMAR EXTEND`
+- wrap every occurrence of OCaml code in actions into braces `{ }`
+
+For instance, code of the form
+```
+GEXTEND Gram
+   GLOBAL: my_entry;
+
+my_entry:
+[ [ x = bar; y = qux -> do_something x y
+  | "("; z = LIST0 my_entry; ")" -> do_other_thing z
+] ];
+END
+```
+should be turned into
+```
+GRAMMAR EXTEND Gram
+   GLOBAL: my_entry;
+
+my_entry:
+[ [ x = bar; y = qux -> { do_something x y }
+  | "("; z = LIST0 my_entry; ")" -> { do_other_thing z }
+] ];
+END
+```
+
+Caveats:
+- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases
+  this as a shorthand for all global entries. Solution: always define a `GLOBAL`
+  section.
+- No complex patterns allowed in token naming. Solution: match on it inside the
+  OCaml quotation.
+
 ## Changes between Coq 8.7 and Coq 8.8
 
 ### Bug tracker
@@ -16,7 +218,7 @@ All the other bugs kept their number.
 
 General deprecation
 
-- All functions marked [@@ocaml.deprecated] in 8.7 have been
+- All functions marked `[@@ocaml.deprecated]` in 8.7 have been
   removed. Please, make sure your plugin is warning-free in 8.7 before
   trying to port it over 8.8.
 
@@ -44,8 +246,8 @@ We changed the type of the following functions:
 
 - `Global.body_of_constant`: same as above.
 
-- `Constrinterp.*` generally, many functions that used to take an
-  `evar_map ref` have been now switched to functions that will work in
+- `Constrinterp.*`: generally, many functions that used to take an
+  `evar_map ref` have now been switched to functions that will work in
   a functional way. The old style of passing `evar_map`s as references
   is not supported anymore.
 
@@ -63,16 +265,21 @@ We have changed the representation of the following types:
 
 Some tactics and related functions now support static configurability, e.g.:
 
-- injectable, dEq, etc. takes an argument ~keep_proofs which,
-  - if None, tells to behave as told with the flag Keep Proof Equalities
-  - if Some b, tells to keep proof equalities iff b is true
+- `injectable`, `dEq`, etc. take an argument `~keep_proofs` which,
+  - if `None`, tells to behave as told with the flag `Keep Proof Equalities`
+  - if `Some b`, tells to keep proof equalities iff `b` is true
 
 Declaration of printers for arguments used only in vernac command
 
-- It should now use "declare_extra_vernac_genarg_pprule" rather than
-  "declare_extra_genarg_pprule", otherwise, a failure at runtime might
+- It should now use `declare_extra_vernac_genarg_pprule` rather than
+  `declare_extra_genarg_pprule`, otherwise, a failure at runtime might
   happen. An alternative is to register the corresponding argument as
-  a value, using "Geninterp.register_val0 wit None".
+  a value, using `Geninterp.register_val0 wit None`.
+
+Types Alias deprecation and type relocation.
+
+- A few type alias have been deprecated, in all cases the message
+  should indicate what the canonical form is.
 
 ### STM API
 
@@ -110,7 +317,7 @@ functions when some given constants are traversed:
 
   * `declare_reduction_effect`: to declare a hook to be applied when some
   constant are visited during the execution of some reduction functions
-  (primarily cbv).
+  (primarily `cbv`).
 
   * `set_reduction_effect`: to declare a constant on which a given effect
   hook should be called.
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index b3d49b7e..764d4829 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -17,12 +17,6 @@ toplevel
 Special components
 ------------------
 
-intf :
-
- Contains mli-only interfaces, many of them providing a.s.t.
- used for dialog bewteen coq components. Ex: Constrexpr.constr_expr
- produced by parsing and transformed by interp.
-
 grammar :
 
  Camlp5 syntax extensions. The file grammar/grammar.cma is used
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
new file mode 100644
index 00000000..8d78559c
--- /dev/null
+++ b/dev/doc/critical-bugs
@@ -0,0 +1,262 @@
+Preliminary compilation of critical bugs in stable releases of Coq
+==================================================================
+  WORK IN PROGRESS WITH SEVERAL OPEN QUESTIONS
+
+
+To add: #7723 (vm_compute universe polymorphism), #7695 (modules and algebraic universes), #7615 (lost functor substitutions)
+
+Typing constructions
+
+  component: "match"
+  summary: substitution missing in the body of a let
+  introduced: ?
+  impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl4
+  impacted development branches: none
+  impacted coqchk versions: ?
+  fixed in: master/trunk/v8.5 (e583a79b5, 22 Nov 2015, Herbelin), v8.4 (525056f1, 22 Nov 2015, Herbelin), v8.3 (4bed0289, 22 Nov 2015, Herbelin)
+  found by: Herbelin
+  exploit: test-suite/success/Case22.v
+  GH issue number: ?
+  risk: ?
+
+  component: fixpoint, guard
+  summary: missing lift in checking guard
+  introduced: probably from V5.10
+  impacted released versions: probably V5-V7, V8.0-V8.0pl4, V8.1-V8.1pl4
+  impacted development branches: v8.0 ?
+  impacted coqchk versions: ?
+  fixed in: master/trunk/v8.2 (ff45afa8, r11646, 2 Dec 2008, Barras), v8.1 (f8e7f273, r11648, 2 Dec 2008, Barras)
+  found by: Barras
+  exploit: test-suite/failure/guard.v
+  GH issue number: none
+  risk: unprobable by chance
+
+  component: cofixpoint, guard
+  summary: de Bruijn indice bug in checking guard of nested cofixpoints
+  introduced: after V6.3.1, before V7.0
+  impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4
+  impacted development branches: none
+  impacted coqchk versions: ?
+  fixed in: master (9f81e2c36, 10 Apr 2014, Dénès), v8.4 (f50ec9e7d, 11 Apr 2014, Dénès), v8.3 (40c0fe7f4, 11 Apr 2014, Dénès), v8.2 (06d66df8c, 11 Apr 2014, Dénès), v8.1 (977afae90, 11 Apr 2014, Dénès), v8.0 (f1d632992, 29 Nov 2015, Herbelin, backport)
+  found by: Dénès
+  exploit: ?
+  GH issue number: none ?
+  risk: ?
+
+  component: inductive types, elimination principle
+  summary: de Bruijn indice bug in computing allowed elimination principle
+  introduced: 23 May 2006, 9c2d70b, r8845, Herbelin (part of universe polymorphism)
+  impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4
+  impacted development branches: none
+  impacted coqchk versions: ?
+  fixed in: master (8a01c3685, 24 Jan 2014, Dénès), v8.4 (8a01c3685, 25 Feb 2014, Dénès), v8.3 (2b3cc4f85, 25 Feb 2014, Dénès), v8.2 (459888488, 25 Feb 2014, Dénès), v8.1 (79aa20872, 25 Feb 2014, Dénès)
+  found by: Dénès
+  exploit: see GH#3211
+  GH issue number: #3211
+  risk: ?
+
+  component: universe subtyping
+  summary: bug in Prop<=Set conversion which made Set identifiable with Prop, preventing a proof-irrelevant interpretation of Prop
+  introduced: V8.2 (bba897d5f, 12 May 2008, Herbelin)
+  impacted released versions: V8.2-V8.2pl2
+  impacted development branches: none
+  impacted coqchk versions: ?
+  fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport)
+  found by: Georgi Guninski
+  exploit: test-suite/bugs/closed/4294.v
+  GH issue number: #4294
+  risk: ?
+
+Module system
+
+  component: modules, universes
+  summary: missing universe constraints in typing "with" clause of a module type
+  introduced: ?
+  impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl6; unclear for V8.2 and previous versions
+  impacted development branches: none
+  impacted coqchk versions: ?
+  fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau)
+  found by: Dénès
+  exploit: test-suite/bugs/closed/4294.v
+  GH issue number: #4294
+  risk: ?
+
+Module system
+
+  component: modules, universes
+  summary: universe constraints for module subtyping not stored in vo files
+  introduced: presumably 8.2 (b3d3b56)
+  impacted released versions: 8.2, 8.3, 8.4
+  impacted development branches: v8.5
+  impacted coqchk versions: none
+  fixed in: v8.2 (c1d9889), v8.3 (8056d02), v8.4 (a07deb4), trunk (0cd0a3e) Mar 5, 2014, Tassi
+  found by: Tassi by running coqchk on the mathematical components library
+  exploit: requires multiple files, no test provided
+  GH issue number: #3243
+  risk: could be exploited by mistake
+
+Universes
+
+  component: template polymorphism
+  summary: issue with two parameters in the same universe level
+  introduced: 23 May 2006, 9c2d70b, r8845, Herbelin
+  impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2
+  impacted development branches: none
+  impacted coqchk versions: ?
+  fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin), 
+  found by: Barras
+  exploit: test-suite/failure/inductive4.v
+  GH issue number: none
+  risk: unlikely to be activated by chance
+
+  component: universe polymorphism
+  summary: universe polymorphism can capture global universes
+  impacted released versions: V8.5 to V8.8
+  impacted coqchk versions: V8.5 to current (NOT FIXED)
+  fixed in: 2385b5c1ef
+  found by: Gaëtan Gilbert
+  exploit: test-suite/misc/poly-capture-global-univs
+  GH issue number: #8341
+  risk: unlikely to be activated by chance (requires a plugin)
+
+Primitive projections
+
+  component: primitive projections, guard condition
+  summary: check of guardedness of extra arguments of primitive projections missing
+  introduced: 6 May 2014, a4043608f, Sozeau
+  impacted released versions: V8.5-V8.5pl2, 
+  impacted development branches: none
+  impacted coqchk versions: ?
+  fixed in: trunk/master/v8.5 (ba00867d5, 25 Jul 2016, Sozeau)
+  found by: Sozeau, by analyzing bug report #4876
+  exploit: to be done (?)
+  GH issue number: #4876
+  risk: consequence of bug found by chance, unlikely to be exploited by chance (MS?)
+
+  component: primitive projections, guard condition
+  summary: records based on primitive projections became possibly recursive without the guard condition being updated
+  introduced: 10 Sep 2014, 6624459e4, Sozeau (?)
+  impacted released versions: V8.5
+  impacted development branches: none
+  impacted coqchk versions: ?
+  fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès)
+  found by: Dénès exploiting bug #4588
+  exploit: test-suite/bugs/closed/4588.v
+  GH issue number: #4588
+  risk: ?
+
+Conversion machines
+
+  component: "lazy machine" (lazy krivine abstract machine)
+  summary: the invariant justifying some optimization was wrong for some combination of sharing side effects
+  introduced: prior to V7.0
+  impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl3
+  impacted development branches: none
+  impacted coqchk versions: (eefe63d52, Barras, 20 May 2008), was in beta-development for 8.2 at this time
+  fixed in: master/trunk/8.2 (f13aaec57/a8b034513, 15 May 2008, Barras), v8.1 (e7611477a, 15 May 2008, Barras), v8.0 (6ed40a8bc, 29 Nov 2016, Herbelin, backport)
+  found by: Gonthier
+  exploit: by Gonthier
+  GH issue number: none
+  risk: unrealistic to be exploited by chance
+
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: collision between constructors when more than 256 constructors in a type
+  introduced: V8.1
+  impacted released versions: V8.1-V8.5pl3, V8.2-V8.2pl2, V8.3-V8.3pl3, V8.4-V8.4pl5
+  impacted development branches: none
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport)
+  found by: Dénès, Pédrot
+  exploit: test-suite/failure/vm-bug4157.v
+  GH issue number: #4157
+  risk: 
+
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: wrong universe constraints
+  introduced: possibly exploitable from V8.1; exploitable at least from V8.5
+  impacted released versions: V8.1-V8.4pl5 unknown, V8.5-V8.5pl3, V8.6-V8.6.1, V8.7.0-V8.7.1
+  impacted development branches: unknown for v8.1-v8.4, none from v8.5
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport)
+  found by: Dénès
+  exploit: test-suite/bugs/closed/6677.v
+  GH issue number: #6677
+  risk: 
+
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: missing pops in executing 31bit arithmetic
+  introduced: V8.5
+  impacted released versions: V8.1-V8.4pl5
+  impacted development branches: v8.1 (probably)
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: master/trunk/v8.5 (a5e04d9dd, 6 Sep 2015, Dénès), v8.4 (d5aa3bf6, 9 Sep 2015, Dénès), v8.3 (5da5d751, 9 Sep 2015, Dénès), v8.2 (369e82d2, 9 Sep 2015, Dénès), 
+  found by: Catalin Hritcu
+  exploit: lost?
+  GH issue number: ?
+  risk: 
+
+  component: "native" conversion machine (translation to OCaml which compiles to native code)
+  summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
+  introduced: V8.5
+  impacted released versions: V8.5-V8.5pl1
+  impacted development branches: none
+  impacted coqchk versions: none (no native computation in coqchk)
+  fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey), 
+  found by: Letouzey, Dénès
+  exploit: lost?
+  GH issue number: ?
+  risk: 
+
+Conflicts with axioms in library
+
+  component: library of real numbers
+  summary: axiom of description and decidability of equality on real numbers in library Reals was inconsistent with impredicative Set
+  introduced: 67c75fa01, 20 Jun 2002
+  impacted released versions: 7.3.1, 7.4
+  impacted coqchk versions: 
+  fixed by deciding to drop impredicativity of Set: bac707973, 28 Oct 2004
+  found by: Herbelin & Werner
+  exploit: need to find the example again
+  GH issue number: no
+  risk: unlikely to be exploited by chance
+
+  component: library of extensional sets, guard condition
+  summary: guard condition was unknown to be inconsistent with propositional extensionality in library Sets
+  introduced: not a bug per se but an incompatibility discovered late
+  impacted released versions: technically speaking from V6.1 with the introduction of the Sets library which was then inconsistent from the very beginning without we knew it
+  impacted coqchk versions: ?
+  fixed by constraining the guard condition: (9b272a8, ccd7546c 28 Oct 2014, Barras, Dénès)
+  found by: Schepler, Dénès, Azevedo de Amorim
+  exploit: ?
+  GH issue number: none
+  risk: unlikely to be exploited by chance (?)
+
+  component: library for axiom of choice and excluded-middle
+  summary: incompatibility axiom of choice and excluded-middle with elimination of large singletons to Set
+  introduced: not a bug but a change of intended "model"
+  impacted released versions: strictly before 8.1
+  impacted coqchk versions: ?
+  fixed by constraining singleton elimination: b19397ed8, r9633, 9 Feb 2007, Herbelin
+  found by: Benjamin Werner
+  exploit:
+  GH issue number: none
+  risk:
+
+There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1).
+
+There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical.
+
+Another non exploitable bug?
+
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: bug in 31bit arithmetic
+  introduced: V8.1
+  impacted released versions: none
+  impacted development branches: 
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: master/trunk/v8.5 (0f8d1b92c, 6 Sep 2015, Dénès)
+  found by: Dénès, from a bug report by Tahina Ramananandro
+  exploit: ?
+  GH issue number: ?
+  risk: 
+
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
index 8f96ac22..77455223 100644
--- a/dev/doc/proof-engine.md
+++ b/dev/doc/proof-engine.md
@@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the
 `Refine.refine` primitive.
 
 ```ocaml
-val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
-(** In [refine typecheck t], [t] is a term with holes under some
+val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+(** In [refine ~typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
@@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
     tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 ```
 
-In a first approximation, we can think of `'a Sigma.run` as
-`evar_map -> 'a * evar_map`. What the function does is first evaluate the
-`Constr.t Sigma.run` argument in the current proof state, and then use the
-resulting term as a filler for the proof under focus. All evars that have been
-created by the invocation of this thunk are then turned into new goals added in
-the order of their creation.
+What the function does is first evaluate the `t` argument in the
+current proof state, and then use the resulting term as a filler for
+the proof under focus. All evars that have been created by the
+invocation of this thunk are then turned into new goals added in the
+order of their creation.
 
 To see how we can use it, let us have a look at an idealized example, the `cut`
 tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]`
@@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order.
 
 ```ocaml
 let cut c =
-  let open Sigma in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     (** In this block, we focus on one goal at a time indicated by gl *)
     let env = Proofview.Goal.env gl in
     (** Get the context of the goal, essentially [Γ] *)
@@ -80,25 +78,22 @@ let cut c =
     let t = mkArrow c (Vars.lift 1 concl) in
     (** Build [X -> A]. Note the lifting of [A] due to being on the right hand
         side of the arrow. *)
-    Refine.refine { run = begin fun sigma ->
+    Refine.refine begin fun sigma ->
       (** All evars generated by this block will be added as goals *)
-      let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in
+      let sigma, f = Evarutil.new_evar env sigma t in
       (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the
           term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity
           substitution for [Γ] is extracted from the [env] argument, so that
           one must be careful to pass the correct context here in order for the
           resulting term to be well-typed. The [p] return value is a proof term
           used to enforce sigma monotonicity. *)
-      let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in
+      let sigma, x = Evarutil.new_evar env sigma c in
       (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return
           [x := Γ ⊢ ?e2{Γ} : X]. *)
       let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in
       (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *)
-      Sigma (r, sigma, p +> q)
-      (** Fills the current hole with [r]. The [p +> q] thingy ensures
-          monotonicity of sigma. *)
-    end }
-  end }
+    end
+  end
 ```
 
 The `Evarutil.new_evar` function is the preferred way to generate evars in
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
new file mode 100644
index 00000000..b33a1cbd
--- /dev/null
+++ b/dev/doc/release-process.md
@@ -0,0 +1,128 @@
+# Release process #
+
+## As soon as the previous version branched off master ##
+
+- [ ] Create a new issue to track the release process where you can copy-paste
+  the present checklist.
+- [ ] Change the version name to the next major version and the magic numbers
+  (see [#7008](https://github.com/coq/coq/pull/7008/files)).
+- [ ] Update the compatibility infrastructure, which consists of doing
+      the following steps.  Note that all but the final step can be
+      performed automatically by
+      [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so
+      long as you have already updated `coq_version` in
+      [`configure.ml`](/configure.ml).
+  + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header
+        from [`dev/header.ml`](/dev/header.ml)
+  + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of
+        `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X.
+  + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions
+        prior to X.X.
+  + [ ] Update
+        [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
+        with the deleted/added files.
+  + [ ] Remove any notations in the standard library which have `compat "W.W"`.
+  + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
+        bumping all the version numbers by one, and update the interpretations
+        of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
+        [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+  + [ ] Update the files
+        [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
+        [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
+        and
+        [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v)
+        by bumping all version numbers by 1.
+  + [ ] Decide what to do about all test-suite files which mention `-compat
+        W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only
+        keep compatibility against the two previous versions)
+- [ ] Put the corresponding alpha tag using `git tag -s`.
+  The `VX.X+alpha` tag marks the first commit to be in `master` and not in the
+  branch of the previous version.
+- [ ] Create the `X.X+beta1` milestone if it did not already exist.
+- [ ] Decide the release calendar with the team (freeze date, beta date, final
+  release date) and put this information in the milestone (using the
+  description and due date fields).
+
+## About one month before the beta ##
+
+- [ ] Create the `X.X.0` milestone and set its due date.
+- [ ] Send an announcement of the upcoming freeze on Coqdev and ask people to
+  remove from the beta milestone what they already know won't be ready on time
+  (possibly postponing to the `X.X.0` milestone for minor bug fixes,
+  infrastructure and documentation updates).
+- [ ] Determine which issues should / must be fixed before the beta, add them
+  to the beta milestone, possibly with a
+  ["priority: blocker"](https://github.com/coq/coq/labels/priority%3A%20blocker)
+  label. Make sure that all these issues are assigned (and that the assignee
+  provides an ETA).
+- [ ] Ping the development coordinator (**@mattam82**) to get him started on
+  the update to the Credits chapter of the reference manual.
+  See also [#7058](https://github.com/coq/coq/issues/7058).
+  The command to get the list of contributors for this version is
+  `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2`
+  (the ordering is approximative as it will misplace people with middle names).
+
+## On the date of the feature freeze ##
+
+- [ ] Create the new version branch `vX.X` and
+  [protect it](https://github.com/coq/coq/settings/branches)
+  (activate the "Protect this branch", "Require pull request reviews before
+  merging" and "Restrict who can push to this branch" guards).
+- [ ] Remove all remaining unmerged feature PRs from the beta milestone.
+- [ ] Start a new project to track PR backporting. The proposed model is to
+  have a "X.X-only PRs" column for the rare PRs on the stable branch, a
+  "Request X.X inclusion" column for the PRs that were merged in `master` that
+  are to be considered for backporting, a "Waiting for CI" column to put the
+  PRs in the process of being backported, and "Shipped in ..." columns to put
+  what was backported. (The release manager is the person responsible for
+  merging PRs that target the version branch and backporting appropriate PRs
+  that are merged into `master`).
+  A message to **@coqbot** in the milestone description tells it to
+  automatically add merged PRs to the "Request X.X inclusion" column.
+- [ ] Delay non-blocking issues to the appropriate milestone and ensure
+  blocking issues are solved. If required to solve some blocking issues,
+  it is possible to revert some feature PRs in the version branch only.
+
+## Before the beta release date ##
+
+- [ ] Ensure the Credits chapter has been updated.
+- [ ] Ensure that an appropriate version of the plugins we will distribute with
+  Coq has been tagged.
+- [ ] Have some people test the recently auto-generated Windows and MacOS
+  packages.
+- [ ] Change the version name from alpha to beta1 (see
+  [#7009](https://github.com/coq/coq/pull/7009/files)).
+  We generally do not update the magic numbers at this point.
+- [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+
+### These steps are the same for all releases (beta, final, patch-level) ###
+
+- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that
+  package managers can start preparing package updates.
+- [ ] Draft a release on GitHub.
+- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and
+  upload them on GitHub.
+- [ ] Prepare a page of news on the website with the link to the GitHub release
+  (see [coq/www#63](https://github.com/coq/www/pull/63)).
+- [ ] Upload the new version of the reference manual to the website.
+  *TODO: setup some continuous deployment for this.*
+- [ ] Merge the website update, publish the release
+  and send annoucement e-mails.
+- [ ] Ping **@Zimmi48** to publish a new version on Zenodo.
+  *TODO: automate this.*
+- [ ] Close the milestone
+
+## At the final release time ##
+
+- [ ] Change the version name to X.X.0 and the magic numbers (see
+  [#7271](https://github.com/coq/coq/pull/7271/files)).
+- [ ] Put the `VX.X.0` tag.
+
+Repeat the generic process documented above for all releases.
+
+- [ ] Switch the default version of the reference manual on the website.
+
+## At the patch-level release time ##
+
+We generally do not update the magic numbers at this point (see
+[`2881a18`](https://github.com/coq/coq/commit/2881a18)).
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
deleted file mode 100644
index c48c2d5d..00000000
--- a/dev/doc/setup.txt
+++ /dev/null
@@ -1,269 +0,0 @@
-This document provides detailed guidance on how to:
-- compile Coq
-- take advantage of Merlin in Emacs
-- enable auto-completion for Ocaml source-code
-- use ocamldebug in Emacs for debugging coqtop
-The instructions were tested with Debian 8.3 (Jessie).
-
-The procedure is somewhat tedious, but the final results are (still) worth the effort.
-
-How to compile Coq
-------------------
-
-Getting build dependencies:
-
-  sudo apt-get install make opam git
-  opam init --comp 4.02.3
-  # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files.
-  
-  source ~/.bashrc
-  
-  # needed if you want to build "coqtop" target
-  opam install camlp5
-  
-  # needed if you want to build "coqide" target
-  sudo apt-get install liblablgtksourceview2-ocaml-dev libgtk2.0-dev libgtksourceview2.0-dev
-  opam install lablgtk
-  
-  # needed if you want to build "doc" target
-  sudo apt-get install texlive-latex-recommended texlive-fonts-extra texlive-math-extra \
-                       hevea texlive-latex-extra latex-xcolor
-
-Cloning Coq:
-
-  # Go to the directory where you want to clone Coq's source-code. E.g.:
-  cd ~/git
-
-  git clone https://github.com/coq/coq.git
-
-Building coqtop:
-
-  cd ~/git/coq
-  git checkout trunk
-  make distclean
-  ./configure -profile devel
-  make clean
-  make -j4 coqide printers
-
-The "-profile devel" enables all options recommended for developers (like
-warnings, support for Merlin, etc).  Moreover Coq is configured so that
-it can be run without installing it (i.e. from the current directory).
-
-Once the compilation is over check if
-- bin/coqtop
-- bin/coqide
-behave as expected.
-
-
-A note about rlwrap
--------------------
-
-When using "rlwrap coqtop" make sure the version of rlwrap is at least
-0.42, otherwise you will get
-
-  rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory
-
-If this happens either update or use an alternate readline wrapper like "ledit".
-
-
-How to install and configure Merlin (for Emacs)
------------------------------------------------
-
-  sudo apt-get install emacs
-
-  opam install tuareg
-  # Follow the advice displayed at the end as how to update your ~/.emacs file.
-  
-  opam install merlin
-  # Follow the advice displayed at the end as how to update your ~/.emacs file.
-
-Then add this:
-
-  (push "~/.opam/4.02.3/share/emacs/site-lisp" load-path)     ; directory containing merlin.el
-  (setq merlin-command "~/.opam/4.02.3/bin/ocamlmerlin")      ; needed only if ocamlmerlin not already in your PATH
-  (autoload 'merlin-mode "merlin" "Merlin mode" t)
-  (add-hook 'tuareg-mode-hook 'merlin-mode)
-  (add-hook 'caml-mode-hook 'merlin-mode)
-  (load "~/.opam/4.02.3/share/emacs/site-lisp/tuareg-site-file")
-  
-  ;; Do not use TABs. These confuse Merlin.
-  (setq-default indent-tabs-mode nil)
-
-to your ~/.emacs file.
-
-Further Emacs configuration when we start it for the first time.
-
-Try to open some *.ml file in Emacs, e.g.:
-
-  cd ~/git/coq
-  emacs toplevel/coqtop.ml &
-
-Emacs display the following strange message:
-
-  The local variables list in ~/git/coq
-  contains values that may be safe (*).
-
-  Do you want to apply it?
-
-Just press "!", i.e. "apply the local variable list, and permanently mark these values (\*) as safe."
-
-Emacs then shows two windows:
-- one window that shows the contents of the "toplevel/coqtop.ml" file
-- and the other window that shows greetings for new Emacs users.
-
-If you do not want to see the second window next time you start Emacs, just check "Never show it again" and click on "Dismiss this startup screen."
-
-The default key-bindings are described here:
-
-  https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch
-
-If you want, you can customize them by replacing the following lines:
-
-  (define-key merlin-map (kbd "C-c C-x") 'merlin-error-next)
-  (define-key merlin-map (kbd "C-c C-l") 'merlin-locate)
-  (define-key merlin-map (kbd "C-c &") 'merlin-pop-stack)
-  (define-key merlin-map (kbd "C-c C-t") 'merlin-type-enclosing)
-
-in the file "~/.opam/4.02.3/share/emacs/site-lisp/merlin.el" with what you want.
-In the text below we assume that you changed the origin key-bindings in the following way:
-
-  (define-key merlin-map (kbd "C-n") 'merlin-error-next)
-  (define-key merlin-map (kbd "C-l") 'merlin-locate)
-  (define-key merlin-map (kbd "C-b") 'merlin-pop-stack)
-  (define-key merlin-map (kbd "C-t") 'merlin-type-enclosing)
-
-Now, when you press <Ctrl+L>, Merlin will show the definition of the symbol in a separate window.
-If you prefer to jump to the definition within the same window, do this:
-
-  <Alt+X> customize-group <ENTER> merlin <ENTER>
-
-    Merlin Locate In New Window
-
-      Value Menu
-
-        Never Open In New Window
-
-      State
-
-        Set For Future Sessions
-
-Testing (Merlin):
-
-  cd ~/git/coq
-  emacs toplevel/coqtop.ml &
-
-Go to the end of the file where you will see the "start" function.
-
-Go to a line where "init_toplevel" function is called.
-
-If you want to jump to the position where that function or datatype under the cursor is defined, press <Ctrl+L>.
-
-If you want to jump back, type: <Ctrl+B>
-
-If you want to learn the type of the value at current cursor's position, type: <Ctrl+T>
-
-
-Enabling auto-completion in emacs
----------------------------------
-
-In Emacs, type: <Alt+M> list-packages <ENTER>
-
-In the list that is displayed, click on "company".
-
-A new window appears where just click on "Install" and then answer "Yes".
-
-These lines:
-
-  (package-initialize)
-  (require 'company)
-  ; Make company aware of merlin
-  (add-to-list 'company-backends 'merlin-company-backend)
-  ; Enable company on merlin managed buffers
-  (add-hook 'merlin-mode-hook 'company-mode)
-  (global-set-key [C-tab] 'company-complete)
-
-then need to be added to your "~/.emacs" file.
-
-Next time when you start emacs and partially type some identifier,
-emacs will offer the corresponding completions.
-Auto-completion can also be manually invoked by typing <Ctrl+TAB>.
-Description of various other shortcuts is here.
-
-  http://company-mode.github.io/
-
-
-Getting along with ocamldebug
------------------------------
-
-The default ocamldebug key-bindings are described here.
-
-  http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec369
-
-If you want, you can customize them by putting the following commands:
-
-  (global-set-key (kbd "<f5>") 'ocamldebug-break)
-  (global-set-key (kbd "<f6>") 'ocamldebug-run)
-  (global-set-key (kbd "<f7>") 'ocamldebug-next)
-  (global-set-key (kbd "<f8>") 'ocamldebug-step)
-  (global-set-key (kbd "<f9>") 'ocamldebug-finish)
-  (global-set-key (kbd "<f10>") 'ocamldebug-print)
-  (global-set-key (kbd "<f12>") 'camldebug)
-
-to your "~/.emacs" file.
-
-Let us try whether ocamldebug in Emacs works for us.
-(If necessary, re-)compile coqtop:
-
-  cd ~/git/coq
-  make -j4 coqide printers
-
-open Emacs:
-
-  emacs toplevel/coqtop.ml &
-
-and type:
-
-  <F12> ../bin/coqtop.byte <ENTER> ../dev/ocamldebug-coq <ENTER>
-
-As a result, a new window is open at the bottom where you should see:
-
-  (ocd)
-
-i.e. an ocamldebug shell.
-
-  1. Switch to the window that contains the "coqtop.ml" file.
-  2. Go to the end of the file.
-  3. Find the definition of the "start" function.
-  4. Go to the "let" keyword that is at the beginning of the first line.
-  5. By pressing <F5> you set a breakpoint to the cursor's position.
-  6. By pressing <F6> you start the bin/coqtop process.
-  7. Then you can:
-     - step over function calls: <F7>
-     - step into function calls: <F8>
-     - or finish execution of the current function until it returns: <F9>.
-
-Other ocamldebug commands, can be typed to the window that holds the ocamldebug shell.
-
-The points at which the execution of Ocaml program can stop are defined here:
-
-  http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec350
-
-
-Installing printers to ocamldebug
----------------------------------
-
-There is a pretty comprehensive set of printers defined for many common data types.
-You can load them by switching to the window holding the "ocamldebug" shell and typing:
-
-  (ocd) source "../dev/db"
-
-
-Some of the functions were you might want to set a breakpoint and see what happens next
----------------------------------------------------------------------------------------
-
-- Coqtop.start : This function is the main entry point of coqtop.
-- Coqtop.parse_args : This function is responsible for parsing command-line arguments.
-- Coqloop.loop : This function implements the read-eval-print loop.
-- Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\
-                         It dispatches the control to specific functions handling different Vernacular command.
-- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command.
diff --git a/dev/doc/translate.txt b/dev/doc/translate.txt
deleted file mode 100644
index 5b372c96..00000000
--- a/dev/doc/translate.txt
+++ /dev/null
@@ -1,495 +0,0 @@
-
-                 How to use the translator
-                 =========================
-
-       (temporary version to be included in the official
-           TeX document describing the translator)
-
-The translator is a smart, robust and powerful tool to improve the
-readibility of your script. The current document describes the
-possibilities of the translator.
-
-In case of problem recompiling the translated files, don't waste time
-to modify the translated file by hand, read first the following
-document telling on how to modify the original files to get a smooth
-uniform safe translation. All 60000 lines of Coq lines on our
-user-contributions server have been translated without any change
-afterwards, and 0,5 % of the lines of the original files (mainly
-notations) had to be modified beforehand to get this result.
-
-Table of contents
------------------
-
-I) Implicit Arguments
- 1) Strict Implicit Arguments 
- 2) Implicit Arguments in standard library
-
-II) Notations
- 1) Translating a V7 notation as it was
- 2) Translating a V7 notation which conflicts with the new syntax
-  a) Associativity conflicts
-  b) Conflicts with other notations
-   b1) A notation hides another notation 
-   b2) A notation conflicts with the V8 grammar
-   b3) My notation is already defined at another level
-  c) How to use V8only with Distfix ?
-  d) Can I overload a notation in V8, e.g. use "*" and "+" ?
- 3) Using the translator to have simplest notations
- 4) Setting the translator to automatically use new notations that
-    wasn't used in old syntax
- 5) Defining a construction and its notation simultaneously
-
-III) Various pitfalls
- 1) New keywords
- 2) Old "Case" and "Match"
- 3) Change of definition or theorem names
- 4) Change of tactic names
-
----------------------------------------------------------------------
-
-I) Implicit Arguments
-   ------------------
-
-1) Strict Implicit Arguments 
-
-  "Set Implicit Arguments" changes its meaning in V8: the default is
-to turn implicit only the arguments that are _strictly_ implicit (or
-rigid), i.e. that remains inferable whatever the other arguments
-are. E.g "x" inferable from "P x" is not strictly inferable since it
-can disappears if "P" is instanciated by a term which erase "x".
-
-  To respect the old semantics, the default behaviour of the
-translator is to replace each occurrence "Set Implicit Arguments" by
-
-  Set Implicit Arguments.
-  Unset Strict Implicits.
-
-  However, you may wish to adopt the new semantics of "Set Implicit
-Arguments" (for instance because you think that the choice of
-arguments it setsimplicit is more "natural" for you). In this case,
-add the option -strict-implicit to the translator.
-
-  Warning: Changing the number of implicit arguments can break the
-notations.  Then use the V8only modifier of Notations.
-
-2) Implicit Arguments in standard library
-
-  Main definitions of standard library have now implicit
-arguments. These arguments are dropped in the translated files. This
-can exceptionally be a source of incompatibilities which has to be
-solved by hand (it typically happens for polymorphic functions applied
-to "nil" or "None").
-
-II) Notations
-    ---------
-
-  Grammar (on constr) and Syntax are no longer supported. Replace them by
-Notation before translation.
-
-  Precedence levels are now from 0 to 200. In V8, the precedence and
-associativity of an operator cannot be redefined. Typical level are
-(refer to the chapter on notations in the Reference Manual for the
-full list):
-
-  <-> : 95                    (no associativity)
-  -> : 90                     (right associativity)
-  \/ : 85                     (right associativity)
-  /\ : 80                     (right associativity)
-  ~ : 75                      (right associativity)
-  =, <, >, <=, >=, <> : 70    (no associativity)
-  +, - : 50                   (left associativity)
-  *, / : 40                   (left associativity)
-  ^ : 30                      (right associativity)
-
-1) Translating a V7 notation as it was
-
-  By default, the translator keeps the associativity given in V7 while
-the levels are mapped according to the following table:
- 
-  the V7 levels             [  0;  1;  2;  3;  4;  5;  6;  7;  8;  9;  10]
-  are resp. mapped in V8 to [  0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100]
-  with predefined assoc     [ No;  L;  R;  L;  L; No;  R;  R;  R; No;   L]
-
-  If this is OK for you, just simply apply the translator.
-
-2) Translating a V7 notation which conflicts with the new syntax
-
-a) Associativity conflict
-
-  Since the associativity of the levels obtained by translating a V7
-level (as shown on table above) cannot be changed, you have to choose
-another level with a compatible associativity.
-
-  You can choose any level between 0 and 200, knowing that the
-standard operators are already set at the levels shown on the list
-above. 
-
-Example 1: Assume you have a notation
-
-Infix NONA 2 "=_S" my_setoid_eq.
-
-By default, the translator moves it to level 30 which is right
-associative, hence a conflict with the expected no associativity.
-
-To solve the problem, just add the "V8only" modifier to reset the
-level and enforce the associativity as follows:
-
-Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).
-
-The translator now knows that it has to translate "=_S" at level 70
-with no associativity.
-
-Rem: 70 is the "natural" level for relations, hence the choice of 70
-here, but any other level accepting a no-associativity would have been
-OK.
-
-Example 2: Assume you have a notation
-
-Infix RIGHTA 1 "o" my_comp.
-
-By default, the translator moves it to level 20 which is left
-associative, hence a conflict with the expected right associativity.
-
-To solve the problem, just add the "V8only" modifier to reset the
-level and enforce the associativity as follows:
-
-Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).
-
-The translator now knows that it has to translate "o" at level 20
-which has the correct "right associativity".
-
-Rem: We assumed here that the user wants a strong precedence for
-composition, in such a way, say, that "f o g + h" is parsed as
-"(f o g) + h". To get "o" binding less than the arithmetical operators,
-an appropriated level would have been close of 70, and below, e.g. 65.
-
-b) Conflicts with other notations
-
-Since the new syntax comes with new keywords and new predefined
-symbols, new conflicts can occur. Again, you can use the option V8only
-to inform the translator of the new syntax to use.
-
-b1) A notation hides another notation 
-
-Rem: use Print Grammar constr in V8 to diagnose the overlap and see the
-section on factorization in the chapter on notations of the Reference
-Manual for hints on how to factorize.
-
-Example:
-
-Notation "{ x }" := (my_embedding x) (at level 1).
-
-overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at
-level 99. The conflicts can be solved by left-factorizing the notation
-as follows:
-
-Notation "{ x }" := (my_embedding x) (at level 1)
-  V8only (at level 0, x at level 99).
-
-b2) A notation conflicts with the V8 grammar.
-
-Again, use the V8only modifier to tell the translator to automatically
-take in charge the new syntax.
-
-Example:
-
-Infix 3 "@" app.
-
-Since "@" is used in the new syntax for deactivating the implicit
-arguments, another symbol has to be used, e.g. "@@". This is done via
-the V8only option as follows:
-
-Infix 3 "@" app V8only "@@" (at level 40, left associativity).
-
-or, alternatively by
-
-Notation "x @ y" := (app x y) (at level 3, left associativity)
-  V8only "x @@ y" (at level 40, left associativity).
-
-b3) My notation is already defined at another level (or with another
-associativity)
-
-In V8, the level and associativity of a given notation can no longer
-be changed. Then, either you adopt the standard reserved levels and
-associativity for this notation (as given on the list above) or you
-change your notation.
-
-- To change the notation, follow the directions in section b2.
-
-- To adopt the standard level, just use V8only without any argument.
-
-Example.
-
-Infix 6 "*" my_mult.
-
-is not accepted as such in V8. Write
-
-Infix 6 "*" my_mult V8only.
-
-to tell the translator to use "*" at the reserved level (i.e. 40 with
-left associativity). Even better, use interpretation scopes (look at
-the Reference Manual).
-
-c) How to use V8only with Distfix ?
-
-You can't, use Notation instead of Distfix.
-
-d) Can I overload a notation in V8, e.g. use "*" and "+" for my own
-algebraic operations ?
-
-Yes, using interpretation scopes (see the corresponding chapter in the
-Reference Manual).
-
-3) Using the translator to have simplest notations
-
-Thanks to the new syntax, * has now the expected left associativity,
-and the symbols <, >, <= and >= are now available.
-
-Thanks to the interpretation scopes, you can overload the
-interpretation of these operators with the default interpretation
-provided in Coq.
-
-This may be a motivation to use the translator to automatically change
-the notations while switching to the new syntax.
-
-See sections b) and d) above for examples.
-
-4) Setting the translator to automatically use new notations that
-wasn't used in old syntax
-
-Thanks to the "Notation" mechanism, defining symbolic notations is
-simpler than in the previous versions of Coq.
-
-Thanks to the new syntax and interpretation scopes, new symbols and
-overloading is available.
-
-This may be a motivation for using the translator to automatically change
-the notations while switching to the new syntax.
-
-Use for that the commands V8Notation and V8Infix.
-
-Examples:
-
-V8Infix "==>" my_relation (at level 65, right associativity).
-
-tells the translator to write an infix "==>" instead of my_relation in
-the translated files.
-
-V8Infix ">=" my_ge.
-
-tells the translator to write an infix ">=" instead of my_ge in the
-translated files and that the level and associativity are the standard
-one (as defined in the chart above).
-
-V8Infix ">=" my_ge : my_scope.
-
-tells the translator to write an infix ">=" instead of my_ge in the
-translated files, that the level and associativity are the standard
-one (as defined in the chart above), but only if scope my_scope is
-open or if a delimiting key is available for "my_scope" (see the
-Reference Manual).
-
-5) Defining a construction and its notation simultaneously
-
-This is permitted by the new syntax. Look at the Reference Manual for
-explanation. The translator is not fully able to take this in charge...
-
-III) Various pitfalls
-    ----------------
-
-1) New keywords
-
-  The following identifiers are new keywords
-
-  "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then";
-  "else"; "return"; "mod"; "at"; "let"; "_"; ".("
-
-  The translator automatically add a "_" to names clashing with a
-keyword, except for files. Hence users may need to rename the files
-whose name clashes with a keyword.
-
-  Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type"
-  were already keywords
-
-2) Old "Case" and "Match"
-
-  "Case" and "Match" are normally automatically translated into
-  "match" or "match" and "fix", but sometimes it fails to do so. It
-  typically fails when the Case or Match is argument of a tactic whose
-  typing context is unknown because of a preceding Intro/Intros, as e.g. in 
-
-     Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
-
-  The solution is then to replace the invocation of the sequence of
-  tactics into several invocation of the elementary tactics as follows
-
-     Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
-          ^^^
-
-3) Change of definition or theorem names
-
-  Type "entier" from fast_integer.v is renamed into "N" by the
-translator. As a consequence, user-defined objects of same name "N"
-are systematically qualified even tough it may not be necessary.  The
-same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST
-TO GIVE].
-
-4) Change of tactics names
-
-  Since tactics names are now lowercase, this can clash with
-user-defined tactic definitions. To pally this, clashing names are
-renamed by adding an extra "_" to their name.
-
-======================================================================
-Main examples for new syntax
-----------------------------
-
-1) Constructions
-
-  Applicative terms don't any longer require to be surrounded by parentheses as
-e.g in
-
-  "x = f y -> S x = S (f y)"
-
-
-  Product is written
-
-     "forall x y : T, U"
-     "forall x y, U"
-     "forall (x y : T) z (v w : V), U"
-     etc.
-
-  Abstraction is written
-
-     "fun x y : T, U"
-     "fun x y, U"
-     "fun (x y : T) z (v w : V), U"
-     etc.
-
-  Pattern-matching is written
-
-     "match x with c1 x1 x2 => t | c2 y as z => u end"
-     "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end"
-     "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with
-         c1 x1 x2, _ => t | c2 y, d z => u end"
-
-     The last example is the new form of what was written
-
-    "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of
-         (c1 x1 x2) _ => t | (c2 y) (d z) => u end"
-
-  Pattern-matching of type with one constructors and no dependencies
-of the arguments in the resulting type can be written
-
-    "let (x,y,z) as u return P u := t in v"
-     
-  Local fixpoints are written
-
-    "fix f (n m:nat) z (x : X) {struct m} : nat := ...
-     with ..."
-
-    and "struct" tells which argument is structurally decreasing.
-
-  Explicitation of implicit arguments is written
-
-     "f @1:=u v @3:=w t"
-     "@f u v w t"
-
-2) Tactics
-
-  The main change is that tactics names are now lowercase. Besides
-this, the following renaming are applied:
-
-  "NewDestruct" -> "destruct"
-  "NewInduction" -> "induction"
-  "Induction" -> "simple induction"
-  "Destruct" -> "simple destruct"
-
-  For tactics with occurrences, the occurrences now comes after and
-  repeated use is separated by comma as in
-
-  "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4"
-  "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4"
-  "Simpl 1 3 e" -> "simpl e at 1 3"
-
-3) Tactic language
-
-  Definitions are now introduced with keyword "Ltac" (instead of
-"Tactic"/"Meta" "Definition") and are implicitly recursive
-("Recursive" is no longer used).
-
-  The new rule for distinguishing terms from ltac expressions is:
-
-  Write "ltac:" in front of any tactic in argument position and
-  "constr:" in front of any construction in head position
-
-4) Vernacular language
-
-a) Assumptions
-
-  The syntax for commands is mainly unchanged. Declaration of
-assumptions is now done as follows
-
-  Variable m : t.
-  Variables m n p : t.
-  Variables (m n : t) (u v : s) (w : r).
-  
-b) Definitions
-
-  Definitions are done as follows
-
-  Definition f m n : t := ... .
-  Definition f m n := ... .
-  Definition f m n := ... : t.
-  Definition f (m n : u) : t := ... .
-  Definition f (m n : u) := ... : t.
-  Definition f (m n : u) := ... .
-  Definition f a b (p q : v) r s (m n : t) : t := ... .
-  Definition f a b (p q : v) r s (m n : t) := ... .
-  Definition f a b (p q : v) r s (m n : t) := ... : t.
-
-c) Fixpoints
-
-  Fixpoints are done this way
-  
-  Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... .
-  Fixpoint f x : v := ... .
-  Fixpoint f (x : t) : v := ... .
-
-  It is possible to give a concrete notation to a fixpoint as follows
-
-  Fixpoint plus (n m:nat) {struct n} : nat as "n + m" :=
-    match n with
-    | O => m
-    | S p => S (p + m)
-    end.
-
-d) Inductive types
-
-  The syntax for inductive types is as follows
-
-  Inductive t (a b : u) (d : e) : v :=
-     c1 : w1 | c2 : w2 | ... .
-
-  Inductive t (a b : u) (d : e) : v :=
-     c1 : w1 | c2 : w2 | ... .
-
-  Inductive t (a b : u) (d : e) : v :=
-     c1 (x y : t) : w1 | c2 (z : r) : w2 | ... .
-
-  As seen in the last example, arguments of the constructors can be
-given before the colon. If the type itself is omitted (allowed only in
-case the inductive type has no real arguments), this yields an
-ML-style notation as follows
-
-  Inductive nat : Set := O | S (n:nat).
-  Inductive bool : Set := true | false.
-
-  It is even possible to define a syntax at the same time, as follows:
-
-  Inductive or (A B:Prop) : Prop as "A \/ B":=
-    | or_introl (a:A) : A \/ B 
-    | or_intror (b:B) : A \/ B.
-
-  Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B).
-  
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 3867d4af..8f9c3171 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -395,7 +395,17 @@ Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect pl
 
 Coq V8.7 beta 2 & released 6 October 2017 & \\
 
-Coq V8.7 & released 18 October 2016 & \\
+Coq V8.7.0 & released 18 October 2017 & \\
+
+Coq V8.7.1 & released 15 December 2017 & \\
+
+Coq V8.7.2 & released 17 February 2018 & \\
+
+Coq V8.8 beta1 & released 19 March 2018 & \\
+
+Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\
+&& \feature{effort towards better documented, better structured ML API}\\
+&& \feature{miscellaneous changes/improvements of existing features}\\
 
 \end{tabular}
 
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index b35571e9..48671c03 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -10,9 +10,9 @@ versions of Proof General.
 
 A somewhat out-of-date description of the async state machine is
 [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md).
-OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli).
+OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml).
 
-Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt).
+Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md).
 
 * [Commands](#commands)
   - [About](#command-about)
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index ee9c8777..cd09b6d3 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -31,4 +31,6 @@ fi
 find . "(" -path ./.git -prune ")" -o -type f -print0 |
     xargs -0 dev/tools/check-eof-newline.sh || CODE=1
 
+dev/tools/check-overlays.sh || CODE=1
+
 exit $CODE
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index f3e60ede..bccd3fef 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -14,18 +14,26 @@
 
 export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
 
-exec $OCAMLDEBUG \
+GUESS_CHECKER=
+for arg in "$@"; do
+    if [ "${arg##*/}" = coqchk.byte ]; then
+        GUESS_CHECKER=1
+    fi
+done
+
+if [ -z "$GUESS_CHECKER" ]; then
+    exec $OCAMLDEBUG \
 	-I $CAMLP5LIB -I +threads \
 	-I $COQTOP \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
-	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
+	-I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
 	-I $COQTOP/library -I $COQTOP/engine \
 	-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
         -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
-        -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
+        -I $COQTOP/plugins/firstorder \
         -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
         -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
         -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
@@ -35,3 +43,11 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
         -I $COQTOP/ide \
 	"$@"
+else
+    exec $OCAMLDEBUG \
+        -I $CAMLP5LIB -I +threads \
+        -I $COQTOP \
+        -I $COQTOP/config -I $COQTOP/clib \
+        -I $COQTOP/lib -I $COQTOP/checker \
+        "$@"
+fi
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index e4359f70..9864fd4d 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -1,11 +1,34 @@
 #!/usr/bin/env bash
 
-# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging]
-
 set -e
 
-PRNUM=$1
-OPTION=$2
+if [[ $# == 0 ]]; then
+    echo "Usage: $0 [--no-conflict] [--no-signature-check] [--stop-before-merging] prnum"
+    exit 1
+fi
+
+while [[ $# -gt 0 ]]; do
+    case "$1" in
+        --no-conflict)
+            NO_CONFLICTS="true"
+            shift
+            ;;
+        --no-signature-check)
+            NO_SIGNATURE_CHECK="true"
+            shift
+            ;;
+        --stop-before-merging)
+            STOP_BEFORE_MERGING="true"
+            shift
+            ;;
+        *)
+            if [[ "$PRNUM" != "" ]]; then
+                echo "PRNUM was already set to $PRNUM and is now being overridden with $1."
+            fi
+            PRNUM="$1"
+            shift
+    esac
+done
 
 if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
     echo "PR #${PRNUM} does not exist."
@@ -14,7 +37,7 @@ fi
 
 SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?")
 git log master --grep "Merge PR #${PRNUM}" --format="%GG"
-if [[ "${SIGNATURE_STATUS}" != "G" ]]; then
+if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then
     echo
     read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r
     echo
@@ -27,9 +50,17 @@ BRANCH=backport-pr-${PRNUM}
 RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../')
 MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/')
 
-if git checkout -b ${BRANCH}; then
+if git checkout -b "${BRANCH}"; then
 
-    if ! git cherry-pick -x ${RANGE}; then
+    if ! git cherry-pick -x "${RANGE}"; then
+        if [[ "$NO_CONFLICTS" == "true" ]]; then
+            git status
+            echo "Conflicts! Aborting..."
+            git cherry-pick --abort
+            git checkout -
+            git branch -d "$BRANCH"
+            exit 1
+        fi
         echo "Please fix the conflicts, then exit."
         bash
         while ! git cherry-pick --continue; do
@@ -50,7 +81,7 @@ else
 
 fi
 
-if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then
     echo
     read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
     echo
@@ -59,12 +90,12 @@ if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
     fi
 fi
 
-if [[ "${OPTION}" == "--stop-before-merging" ]]; then
+if [[ "$STOP_BEFORE_MERGING" == "true" ]]; then
     exit 0
 fi
 
-git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
-git branch -d ${BRANCH}
+git merge -S --no-ff "${BRANCH}" -m "${MESSAGE}"
+git branch -d "${BRANCH}"
 
 # To-Do:
 # - Support for backporting a PR before it is merged
diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh
new file mode 100755
index 00000000..33a9ff05
--- /dev/null
+++ b/dev/tools/check-overlays.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+for f in $(git ls-files "dev/ci/user-overlays/")
+do
+    if ! ([[ "$f" = dev/ci/user-overlays/README.md ]] || [[ "$f" == *.sh ]])
+    then
+        >&2 echo "Bad overlay '$f'."
+        >&2 echo "User overlays need to have extension .sh to be picked up!"
+        exit 1
+    fi
+done
diff --git a/dev/tools/check-owners-pr.sh b/dev/tools/check-owners-pr.sh
new file mode 100755
index 00000000..d2910279
--- /dev/null
+++ b/dev/tools/check-owners-pr.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env sh
+
+usage() {
+    { echo "usage: $0 PR [ARGS]..."
+      echo "A wrapper around check-owners.sh to check owners for a PR."
+      echo "Assumes upstream is the canonical Coq repository."
+      echo "Assumes the PR is against master."
+      echo
+      echo "  PR: PR number"
+      echo "  ARGS: passed through to check-owners.sh"
+    } >&2
+}
+
+case "$1" in
+    "--help"|"-h")
+        usage
+        if [ $# = 1 ]; then exit 0; else exit 1; fi;;
+    "")
+        usage
+        exit 1;;
+esac
+
+PR="$1"
+shift
+
+# this puts both refs in the FETCH_HEAD file but git rev-parse will use the first
+git fetch upstream "+refs/pull/$PR/head" master
+
+head=$(git rev-parse FETCH_HEAD)
+base=$(git merge-base upstream/master "$head")
+
+git diff --name-only -z "$base" "$head" | xargs -0 dev/tools/check-owners.sh "$@"
diff --git a/dev/tools/check-owners.sh b/dev/tools/check-owners.sh
new file mode 100755
index 00000000..1a97508a
--- /dev/null
+++ b/dev/tools/check-owners.sh
@@ -0,0 +1,138 @@
+#!/usr/bin/env bash
+
+# Determine CODEOWNERS of the files given in argument
+# For a given commit range:
+# git diff --name-only -z COMMIT1 COMMIT2 | xargs -0 dev/tools/check-owners.sh [opts]
+
+# NB: gitignore files will be messed up if you interrupt the script.
+# You should be able to just move the .gitignore.bak files back manually.
+
+usage() {
+    { echo "usage: $0 [--show-patterns] [--owner OWNER] [FILE]..."
+      echo "  --show-patterns: instead of printing file names print the matching patterns (more compact)"
+      echo "  --owner: show only files/patterns owned by OWNER (use Nobody to see only non-owned files)"
+    } >&2
+}
+
+case "$1" in
+    "--help"|"-h")
+        usage
+        if [ $# = 1 ]; then exit 0; else exit 1; fi
+esac
+
+if ! [ -e .github/CODEOWNERS ]; then
+    >&2 echo "No CODEOWNERS set up or calling from wrong directory."
+    exit 1
+fi
+
+files=()
+show_patterns=false
+
+target_owner=""
+
+while [[ "$#" -gt 0 ]]; do
+    case "$1" in
+        "--show-patterns")
+            show_patterns=true
+            shift;;
+        "--owner")
+            if [[ "$#" = 1 ]]; then
+                >&2 echo "Missing argument to --owner"
+                usage
+                exit 1
+            elif [[ "$target_owner" != "" ]]; then
+                >&2 echo "Only one --owner allowed"
+                usage
+                exit 1
+            fi
+            target_owner="$2"
+            shift 2;;
+        *)
+            files+=("$@")
+            break;;
+    esac
+done
+
+# CODEOWNERS uses .gitignore patterns so we want to use git to parse it
+# The only available tool for that is git check-ignore
+# However it provides no way to use alternate .gitignore files
+# so we rename them temporarily
+
+find . -name .gitignore -print0 | while IFS= read -r -d '' f; do
+    if [ -e "$f.bak" ]; then
+        >&2 echo "$f.bak exists!"
+        exit 1
+    else
+        mv "$f" "$f.bak"
+    fi
+done
+
+# CODEOWNERS is not quite .gitignore patterns:
+# after the pattern is the owner (space separated)
+# git would interpret that as a big pattern containing spaces
+# so we create a valid .gitignore by removing all but the first field
+
+while read -r pat _; do
+    printf '%s\n' "$pat" >> .gitignore
+done < .github/CODEOWNERS
+
+# associative array [file => owner]
+declare -A owners
+
+for f in "${files[@]}"; do
+    data=$(git check-ignore --verbose --no-index "./$f")
+    code=$?
+
+    if [[ "$code" = 1 ]] || ! [[ "$data" =~ .gitignore:.* ]] ; then
+        # no match, or match from non tracked gitignore (eg global gitignore)
+        if [ "$target_owner" != "" ] && [ "$target_owner" != Nobody ] ; then
+            owner=""
+        else
+            owner="Nobody"
+            pat="$f" # no patterns for unowned files
+        fi
+    else
+        # data looks like [.gitignore:$line:$pattern $file]
+        # extract the line to look it up in CODEOWNERS
+        data=${data#'.gitignore:'}
+        line=${data%%:*}
+
+        # NB: supports multiple owners
+        # Does not support secondary owners declared in comment
+        read -r pat fowners < <(sed "${line}q;d" .github/CODEOWNERS)
+
+        owner=""
+        if [ "$target_owner" != "" ]; then
+            for o in $fowners; do # do not quote: multiple owners possible
+                if [ "$o" = "$target_owner" ]; then
+                    owner="$o"
+                fi
+            done
+        else
+            owner="$fowners"
+        fi
+    fi
+
+    if [ "$owner" != "" ]; then
+        if $show_patterns; then
+            owners[$pat]="$owner"
+        else
+            owners[$f]="$owner"
+        fi
+    fi
+done
+
+for f in "${!owners[@]}"; do
+    printf '%s: %s\n' "$f" "${owners[$f]}"
+done | sort -k 2 -k 1 # group by owner
+
+# restore gitignore files
+rm .gitignore
+find . -name .gitignore.bak -print0 | while IFS= read -r -d '' f; do
+    base=${f%.bak}
+    if [ -e "$base" ]; then
+        >&2 echo "$base exists!"
+    else
+        mv "$f" "$base"
+    fi
+done
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 62fdaec8..ec72f965 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -23,7 +23,7 @@
 
 ;; If you load this file from a git repository, checking out an old
 ;; commit will make it disappear and cause errors for your Emacs
-;; startup. To ignore those errors use (require 'coqdev nil t). If you
+;; startup.  To ignore those errors use (require 'coqdev nil t).  If you
 ;; check out a malicious commit Emacs startup would allow it to run
 ;; arbitrary code, to avoid this you can copy coqdev.el to any
 ;; location and adjust the load path accordingly (of course if you run
@@ -33,7 +33,7 @@
 
 (defun coqdev-default-directory ()
   "Return the Coq repository containing `default-directory'."
-  (let ((dir (locate-dominating-file default-directory "META.coq")))
+  (let ((dir (locate-dominating-file default-directory "META.coq.in")))
     (when dir (expand-file-name dir))))
 
 (defun coqdev-setup-compile-command ()
@@ -103,5 +103,48 @@ Note that this function is executed before _Coqproject is read if it exists."
      2 (3 . 4) (5 . 6)))
   (add-to-list 'compilation-error-regexp-alist 'coq-backtrace))
 
+(defvar bug-reference-bug-regexp)
+(defvar bug-reference-url-format)
+(defun coqdev-setup-bug-reference-mode ()
+  "Setup `bug-reference-bug-regexp' and `bug-reference-url-format' for Coq.
+
+This does not enable `bug-reference-mode'."
+  (let ((dir (coqdev-default-directory)))
+    (when dir
+      (setq-local bug-reference-bug-regexp "#\\(?2:[0-9]+\\)")
+      (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s"))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode)
+
+(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end)
+  "Add LEFT and RIGHT around the BEG..END.
+Leave the point after RIGHT.  BEG and END default to the bounds
+of the current region.  Leave point OFFSET characters after the
+left quote (if OFFSET is nil, leave the point after the right
+quote)."
+  (unless beg
+    (if (region-active-p)
+        (setq beg (region-beginning) end (region-end))
+      (setq beg (point) end nil)))
+  (save-excursion
+    (goto-char (or end beg))
+    (insert right))
+  (save-excursion
+    (goto-char beg)
+    (insert left))
+  (if (and end (not offset)) ;; Second test handles the ::`` case
+      (goto-char (+ end (length left) (length right)))
+    (goto-char (+ beg (or offset (length left))))))
+
+(defun coqdev-sphinx-rst-coq-action ()
+  "Insert a Sphinx role template or quote the current region."
+  (interactive)
+  (pcase (read-char "Command [gntm:`]?")
+    (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`"))
+    (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`"))
+    (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`"))
+    (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`"))
+    (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1))
+    (?` (coqdev-sphinx-quote-coq-refman-region "``" "``"))))
+
 (provide 'coqdev)
 ;;; coqdev ends here
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 9f24960f..320ef6ed 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -1,50 +1,210 @@
 #!/usr/bin/env bash
 
 set -e
+set -o pipefail
 
-# This script depends (at least) on git and jq.
-# It should be used like this: dev/tools/merge-pr.sh /PR number/
-
-#TODO: check arguments and show usage if relevant
-
-PR=$1
+API=https://api.github.com/repos/coq/coq
+OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq"
+OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq"
 
-CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
-REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
-git fetch "$REMOTE" "refs/pull/$PR/head"
+# This script depends (at least) on git (>= 2.7) and jq.
+# It should be used like this: dev/tools/merge-pr.sh /PR number/
 
-API=https://api.github.com/repos/coq/coq
+# Set SLOW_CONF to have the confirmation output wait for a newline
+# E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/
+if [ -z ${SLOW_CONF+x} ]; then
+    QUICK_CONF="-n 1"
+else
+    QUICK_CONF=""
+fi
 
-BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
+RED="\033[31m"
+RESET="\033[0m"
+GREEN="\033[32m"
+BLUE="\033[34m"
+YELLOW="\033[33m"
+info() {
+  echo -e "${GREEN}info:${RESET} $1 ${RESET}"
+}
+error() {
+  echo -e "${RED}error:${RESET} $1 ${RESET}"
+}
+warning() {
+  echo -e "${YELLOW}warning:${RESET} $1 ${RESET}"
+}
 
-COMMIT=$(git rev-parse FETCH_HEAD)
-STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
+check_util() {
+if ! command -v "$1" > /dev/null 2>&1; then
+  error "this script requires the $1 command line utility"
+  exit 1
+fi
+}
 
-if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
-  echo "Wrong base branch"
-  read -p "Bypass? [y/N] " -n 1 -r
+ask_confirmation() {
+  read -p "Continue anyway? [y/N] " $QUICK_CONF -r
   echo
   if [[ ! $REPLY =~ ^[Yy]$ ]]
   then
     exit 1
   fi
+}
+
+check_util jq
+check_util curl
+check_util git
+check_util gpg
+
+# command line parsing
+
+if [ $# != 1 ]; then
+  error "usage: $0 PR-number"
+  exit 1
+fi
+
+if [[ "$1" =~ ^[1-9][0-9]*$ ]]; then
+  PR=$1
+else
+  error "$1 is not a number"
+  exit 1
+fi
+
+# Fetching PR metadata
+
+PRDATA=$(curl -s "$API/pulls/$PR")
+
+TITLE=$(echo "$PRDATA" | jq -r '.title')
+info "title for PR $PR is ${BLUE}$TITLE"
+
+BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label')
+info "PR $PR targets branch ${BLUE}$BASE_BRANCH"
+
+CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+info "you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH"
+
+REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
+if [ -z "$REMOTE" ]; then
+  error "branch ${BLUE}$CURRENT_LOCAL_BRANCH${RESET} has not associated remote"
+  error "don't know where to fetch the PR from"
+  error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH"
+  exit 1
+fi
+REMOTE_URL=$(git remote get-url "$REMOTE" --all)
+if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \
+   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \
+   [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}" ] && \
+   [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \
+   [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \
+   [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then
+  error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
+  error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL"
+  error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
+  ask_confirmation
+fi
+info "remote for $CURRENT_LOCAL_BRANCH is ${BLUE}$REMOTE"
+
+info "fetching from $REMOTE the PR"
+git remote update "$REMOTE"
+if ! git ls-remote "$REMOTE" | grep pull >/dev/null; then
+  error "remote $REMOTE is not configured to fetch pull requests"
+  error "run: git config remote.$REMOTE.fetch +refs/pull/*/head:refs/remotes/$REMOTE/pr/*"
+  exit 1
+fi
+git fetch "$REMOTE" "refs/pull/$PR/head"
+COMMIT=$(git rev-parse FETCH_HEAD)
+info "commit for PR $PR is ${BLUE}$COMMIT"
+
+# Sanity check: merge to a different branch
+
+if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
+  error "PR requests merge in ${BLUE}$BASE_BRANCH${RESET} but you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH"
+  ask_confirmation
 fi;
 
-if [ "$STATUS" != "success" ]; then
-  echo "CI status is \"$STATUS\""
-  read -p "Bypass? [y/N] " -n 1 -r
-  echo
-  if [[ ! $REPLY =~ ^[Yy]$ ]]
-  then
-    exit 1
-  fi
+# Sanity check: the local branch is up-to-date with upstream
+
+LOCAL_BRANCH_COMMIT=$(git rev-parse HEAD)
+UPSTREAM_COMMIT=$(git rev-parse @{u})
+if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then
+
+    # Is it just that the upstream branch is behind?
+    # It could just be that we merged other PRs and we didn't push yet
+
+    if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then
+        warning "Your branch is ahead of ${REMOTE}."
+        warning "You should see this warning only if you've just merged another PR and did not push yet."
+        ask_confirmation
+    else
+        error "Local branch is not up-to-date with ${REMOTE}."
+        error "Pull before merging."
+        ask_confirmation
+    fi
+fi
+
+# Sanity check: PR has an outdated version of CI
+
+BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha')
+CI_FILES=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml")
+
+if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
+then
+    warning "This PR didn't run with the latest version of CI."
+    warning "It is probably a good idea to ask for a rebase."
+    read -p "Do you want to see the diff? [Y/n] " $QUICK_CONF -r
+    echo
+    if [[ ! $REPLY =~ ^[Nn]$ ]]
+    then
+        git diff "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
+    fi
+    ask_confirmation
+fi
+
+# Sanity check: CI failed
+
+STATUS=$(curl -s "$API/commits/$COMMIT/status")
+
+if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then
+  error "CI unsuccessful on ${BLUE}$(echo "$STATUS" |
+    jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')"
+  ask_confirmation
 fi;
 
-git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e
+# Sanity check: has labels named "needs:"
+
+NEEDS_LABELS=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)')
+if [ "$NEEDS_LABELS" != "[]" ]; then
+  error "needs:something labels still present: ${BLUE}$NEEDS_LABELS"
+  ask_confirmation
+fi
+
+# Sanity check: has milestone
+
+MILESTONE=$(echo "$PRDATA" | jq -rc '.milestone.title')
+if [ "$MILESTONE" = "null" ]; then
+  error "no milestone set, please set one"
+  ask_confirmation
+fi
+
+# Sanity check: has kind
+
+KIND=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)')
+if [ "$KIND" = "[]" ]; then
+  error "no kind:something label set, please set one"
+  ask_confirmation
+fi
+
+# Sanity check: user.signingkey
+if [ -z "$(git config user.signingkey)" ]; then
+  warning "git config user.signingkey is empty"
+  warning "gpg will guess a key out of your git config user.* data"
+fi
+
+info "merging"
+git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e
 
 # TODO: improve this check
-if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
-  echo "******************************************"
-  echo "** WARNING: does this PR have overlays? **"
-  echo "******************************************"
+if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then
+  warning "this PR may have overlays (sorry the check is not perfect)"
+  warning "if it has overlays please check the following:"
+  warning "- each overlay has a corresponding open PR on the upstream repo"
+  warning "- after merging please notify the upstream they can merge the PR"
 fi
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index dfa95bac..ad2f2f93 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -5,6 +5,8 @@
 
 set -e
 
+dev/tools/check-overlays.sh
+
 if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh ||
         ! git diff-index --check --cached HEAD >/dev/null 2>&1 ;
 then
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
new file mode 100755
index 00000000..7c8b9f02
--- /dev/null
+++ b/dev/tools/update-compat.py
@@ -0,0 +1,341 @@
+#!/usr/bin/env python
+from __future__ import with_statement
+import os, re, sys
+
+# Obtain the absolute path of the script being run.  By assuming that
+# the script lives in dev/tools/, and basing all calls on the path of
+# the script, rather than the current working directory, we can be
+# robust to users who choose to run the script from any location.
+SCRIPT_PATH = os.path.dirname(os.path.realpath(__file__))
+ROOT_PATH = os.path.realpath(os.path.join(SCRIPT_PATH, '..', '..'))
+CONFIGURE_PATH = os.path.join(ROOT_PATH, 'configure.ml')
+HEADER_PATH = os.path.join(ROOT_PATH, 'dev', 'header.ml')
+DEFAULT_NUMBER_OF_OLD_VERSIONS = 2
+EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n'
+FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli')
+FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml')
+COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
+G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
+DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
+BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', '4798.v')
+TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
+                         for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
+TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current')
+# sanity check that we are where we think we are
+assert(os.path.normpath(os.path.realpath(SCRIPT_PATH)) == os.path.normpath(os.path.realpath(os.path.join(ROOT_PATH, 'dev', 'tools'))))
+assert(os.path.exists(CONFIGURE_PATH))
+
+def get_header():
+    with open(HEADER_PATH, 'r') as f: return f.read()
+
+HEADER = get_header()
+
+def get_version(cur_version=None):
+    if cur_version is not None: return cur_version
+    with open(CONFIGURE_PATH, 'r') as f:
+        for line in f.readlines():
+            found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
+            if len(found) > 0:
+                return found[0]
+    raise Exception("No line 'let coq_version = \"X.X' found in %s" % os.path.relpath(CONFIGURE_PATH, ROOT_PATH))
+
+def compat_name_to_version_name(compat_file_name):
+    assert(compat_file_name.startswith('Coq') and compat_file_name.endswith('.v'))
+    v = compat_file_name[len('Coq'):][:-len('.v')]
+    assert(len(v) == 2 or (len(v) >= 2 and v[0] in ('8', '9'))) # we'll have to change this scheme when we hit Coq 10.*
+    return '%s.%s' % (v[0], v[1:])
+
+def version_name_to_compat_name(v, ext='.v'):
+    return 'Coq%s%s%s' % tuple(v.split('.') + [ext])
+
+# returns (lines of compat files, lines of not compat files
+def get_doc_index_lines():
+    with open(DOC_INDEX_PATH, 'r') as f:
+        lines = f.readlines()
+    return (tuple(line for line in lines if 'theories/Compat/Coq' in line),
+            tuple(line for line in lines if 'theories/Compat/Coq' not in line))
+
+COMPAT_INDEX_LINES, DOC_INDEX_LINES = get_doc_index_lines()
+
+def version_to_int_pair(v):
+    return tuple(map(int, v.split('.')))
+
+def get_known_versions():
+    # We could either get the files from the doc index, or from the
+    # directory list.  We assume that the doc index is more
+    # representative.  If we wanted to use the directory list, we
+    # would do:
+    # compat_files = os.listdir(os.path.join(ROOT_PATH, 'theories', 'Compat'))
+    compat_files = re.findall(r'Coq[^\.]+\.v', '\n'.join(COMPAT_INDEX_LINES))
+    return tuple(sorted((compat_name_to_version_name(i) for i in compat_files if i.startswith('Coq') and i.endswith('.v')), key=version_to_int_pair))
+
+def get_new_versions(known_versions, **args):
+    if args['cur_version'] in known_versions:
+        assert(known_versions[-1] == args['cur_version'])
+        assert(len(known_versions) == args['number_of_compat_versions'])
+        return known_versions
+    assert(len(known_versions) >= args['number_of_old_versions'])
+    return tuple(list(known_versions[-args['number_of_old_versions']:]) + [args['cur_version']])
+
+def update_compat_files(old_versions, new_versions, assert_unchanged=False, **args):
+    for v in old_versions:
+        if v not in new_versions:
+            compat_file = os.path.join('theories', 'Compat', version_name_to_compat_name(v))
+            if not assert_unchanged:
+                print('Removing %s...' % compat_file)
+                compat_path = os.path.join(ROOT_PATH, compat_file)
+                os.rename(compat_path, compat_path + '.bak')
+            else:
+                raise Exception('%s exists!' % compat_file)
+    for v, next_v in zip(new_versions, list(new_versions[1:]) + [None]):
+        compat_file = os.path.join('theories', 'Compat', version_name_to_compat_name(v))
+        compat_path = os.path.join(ROOT_PATH, compat_file)
+        if not os.path.exists(compat_path):
+            print('Creating %s...' % compat_file)
+            contents = HEADER + (EXTRA_HEADER % v)
+            if next_v is not None:
+                contents += '\nRequire Export Coq.Compat.%s.\n' % version_name_to_compat_name(next_v, ext='')
+            if not assert_unchanged:
+                with open(compat_path, 'w') as f:
+                    f.write(contents)
+                print(r"Don't forget to 'git add %s'!" % compat_file)
+            else:
+                raise Exception('%s does not exist!' % compat_file)
+        else:
+            # print('Checking %s...' % compat_file)
+            with open(compat_path, 'r') as f:
+                contents = f.read()
+            header = HEADER + (EXTRA_HEADER % v)
+            if not contents.startswith(HEADER):
+                raise Exception("Invalid header in %s; does not match %s" % (compat_file, os.path.relpath(HEADER_PATH, ROOT_PATH)))
+            if not contents.startswith(header):
+                raise Exception("Invalid header in %s; missing line %s" % (compat_file, EXTRA_HEADER.strip('\n') % v))
+            if next_v is not None:
+                line = 'Require Export Coq.Compat.%s.' % version_name_to_compat_name(next_v, ext='')
+                if ('\n%s\n' % line) not in contents:
+                    if not contents.startswith(header + '\n'):
+                        contents = contents.replace(header, header + '\n')
+                    contents = contents.replace(header, '%s\n%s' % (header, line))
+                    if not assert_unchanged:
+                        print('Updating %s...' % compat_file)
+                        with open(compat_path, 'w') as f:
+                            f.write(contents)
+                    else:
+                        raise Exception('Compat file %s is missing line %s' % (compat_file, line))
+
+def update_compat_versions_type_line(new_versions, contents, relpath):
+    compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current'])
+    new_compat_line = 'type compat_version = %s' % compat_version_string
+    new_contents = re.sub(r'^type compat_version = .*$', new_compat_line, contents, flags=re.MULTILINE)
+    if new_compat_line not in new_contents:
+        raise Exception("Could not find 'type compat_version =' in %s" % relpath)
+    return new_contents
+
+def update_version_compare(new_versions, contents, relpath):
+    first_line = 'let version_compare v1 v2 = match v1, v2 with'
+    new_lines = [first_line]
+    for v in new_versions[:-1]:
+        V = 'V%s_%s' % tuple(v.split('.'))
+        new_lines.append('  | %s, %s -> 0' % (V, V))
+        new_lines.append('  | %s, _ -> -1' % V)
+        new_lines.append('  | _, %s -> 1' % V)
+    new_lines.append('  | Current, Current -> 0')
+    new_lines = '\n'.join(new_lines)
+    new_contents = re.sub(first_line + '.*' + 'Current, Current -> 0', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
+    if new_lines not in new_contents:
+        raise Exception('Could not find version_compare in %s' % relpath)
+    return new_contents
+
+def update_pr_version(new_versions, contents, relpath):
+    first_line = 'let pr_version = function'
+    new_lines = [first_line]
+    for v in new_versions[:-1]:
+        V = 'V%s_%s' % tuple(v.split('.'))
+        new_lines.append('  | %s -> "%s"' % (V, v))
+    new_lines.append('  | Current -> "current"')
+    new_lines = '\n'.join(new_lines)
+    new_contents = re.sub(first_line + '.*' + 'Current -> "current"', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
+    if new_lines not in new_contents:
+        raise Exception('Could not find pr_version in %s' % relpath)
+    return new_contents
+
+def update_add_compat_require(new_versions, contents, relpath):
+    first_line = 'let add_compat_require opts v ='
+    new_lines = [first_line, '  match v with']
+    for v in new_versions[:-1]:
+        V = 'V%s_%s' % tuple(v.split('.'))
+        new_lines.append('  | Flags.%s -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % (V, version_name_to_compat_name(v, ext='')))
+    new_lines.append('  | Flags.Current -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % version_name_to_compat_name(new_versions[-1], ext=''))
+    new_lines = '\n'.join(new_lines)
+    new_contents = re.sub(first_line + '.*' + 'Flags.Current -> add_vo_require opts "Coq.Compat.[^"]+" None .Some false.', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
+    if new_lines not in new_contents:
+        raise Exception('Could not find add_compat_require in %s' % relpath)
+    return new_contents
+
+def update_parse_compat_version(new_versions, contents, relpath, **args):
+    line_count = args['number_of_compat_versions']+2 # 1 for the first line, 1 for the invalid flags
+    first_line = 'let parse_compat_version = let open Flags in function'
+    old_function_lines = contents[contents.index(first_line):].split('\n')[:line_count]
+    if re.match(r'^  \| \([0-9 "\.\|]*\) as s ->$', old_function_lines[-1]) is None:
+        raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions' % (line_count, relpath))
+    all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines))
+    invalid_versions = tuple(i for i in all_versions if i not in new_versions)
+    new_function_lines = [first_line]
+    for v, V in reversed(list(zip(new_versions, ['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']))):
+        new_function_lines.append('  | "%s" -> %s' % (v, V))
+    new_function_lines.append('  | (%s) as s ->' % ' | '.join('"%s"' % v for v in invalid_versions))
+    new_lines = '\n'.join(new_function_lines)
+    new_contents = contents.replace('\n'.join(old_function_lines), new_lines)
+    if new_lines not in new_contents:
+        raise Exception('Could not find parse_compat_version in %s' % relpath)
+    return new_contents
+
+def check_no_old_versions(old_versions, new_versions, contents, relpath):
+    for v in old_versions:
+        if v not in new_versions:
+            V = 'V%s_%s' % tuple(v.split('.'))
+            if V in contents:
+                raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath))
+
+def update_if_changed(contents, new_contents, path, assert_unchanged=False, **args):
+    if contents != new_contents:
+        if not assert_unchanged:
+            print('Updating %s...' % os.path.relpath(path, ROOT_PATH))
+            with open(path, 'w') as f:
+                f.write(new_contents)
+        else:
+            raise Exception('%s changed!' % os.path.relpath(path, ROOT_PATH))
+
+def update_flags_mli(old_versions, new_versions, **args):
+    with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read()
+    new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
+    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
+    update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args)
+
+def update_flags_ml(old_versions, new_versions, **args):
+    with open(FLAGS_ML_PATH, 'r') as f: contents = f.read()
+    new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
+    new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
+    new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
+    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
+    update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args)
+
+def update_coqargs_ml(old_versions, new_versions, **args):
+    with open(COQARGS_ML_PATH, 'r') as f: contents = f.read()
+    new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
+    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
+    update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args)
+
+def update_g_vernac(old_versions, new_versions, **args):
+    with open(G_VERNAC_PATH, 'r') as f: contents = f.read()
+    new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args)
+    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH))
+    update_if_changed(contents, new_contents, G_VERNAC_PATH, **args)
+
+def update_flags(old_versions, new_versions, **args):
+    update_flags_mli(old_versions, new_versions, **args)
+    update_flags_ml(old_versions, new_versions, **args)
+    update_coqargs_ml(old_versions, new_versions, **args)
+    update_g_vernac(old_versions, new_versions, **args)
+
+def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, **args):
+    assert(len(new_versions) == len(test_suite_paths))
+    assert(len(new_versions) == len(test_suite_descriptions))
+    for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)):
+        if not os.path.exists(path):
+            raise Exception('Could not find existing file %s' % os.path.relpath(path, ROOT_PATH))
+        if '%s' in descr: descr = descr % v
+        with open(path, 'r') as f: contents = f.read()
+        lines = ['(* -*- coq-prog-args: ("-compat" "%s") -*- *)' % v,
+                 '(** Check that the %s compatibility flag actually requires the relevant modules. *)' % descr]
+        for imp_v in reversed(new_versions[i:]):
+            lines.append('Import Coq.Compat.%s.' % version_name_to_compat_name(imp_v, ext=''))
+        lines.append('')
+        new_contents = '\n'.join(lines)
+        update_if_changed(contents, new_contents, path, **args)
+
+def update_doc_index(new_versions, **args):
+    with open(DOC_INDEX_PATH, 'r') as f: contents = f.read()
+    firstline = '    theories/Compat/AdmitAxiom.v'
+    new_contents = ''.join(DOC_INDEX_LINES)
+    if firstline not in new_contents:
+        raise Exception("Could not find line '%s' in %s" % (firstline, os.path.relpath(DOC_INDEX_PATH, ROOT_PATH)))
+    extra_lines = ['    theories/Compat/%s' % version_name_to_compat_name(v) for v in new_versions]
+    new_contents = new_contents.replace(firstline, '\n'.join([firstline] + extra_lines))
+    update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args)
+
+def update_bug_4789(new_versions, **args):
+    # we always update this compat notation to oldest
+    # currently-supported compat version, which should never be the
+    # current version
+    with open(BUG_4798_PATH, 'r') as f: contents = f.read()
+    new_contents = r"""Check match 2 with 0 => 0 | S n => n end.
+Notation "|" := 1 (compat "%s").
+Check match 2 with 0 => 0 | S n => n end. (* fails *)
+""" % new_versions[0]
+    update_if_changed(contents, new_contents, BUG_4798_PATH, **args)
+
+def update_compat_notations_in(old_versions, new_versions, contents):
+    for v in old_versions:
+        if v not in new_versions:
+            reg = re.compile(r'^[ \t]*(?:Notation|Infix)[^\n]*?compat "%s"[^\n]*?\n' % v, flags=re.MULTILINE)
+            contents = re.sub(r'^[ \t]*(?:Notation|Infix)[^\n]*?compat "%s"[^\n]*?\n' % v, '', contents, flags=re.MULTILINE)
+    return contents
+
+def update_compat_notations(old_versions, new_versions, **args):
+    for root, dirs, files in os.walk(os.path.join(ROOT_PATH, 'theories')):
+        for fname in files:
+            if not fname.endswith('.v'): continue
+            with open(os.path.join(root, fname), 'r') as f: contents = f.read()
+            new_contents = update_compat_notations_in(old_versions, new_versions, contents)
+            update_if_changed(contents, new_contents, os.path.join(root, fname), **args)
+
+def display_git_grep(old_versions, new_versions):
+    Vs = ['V%s_%s' % tuple(v.split('.')) for v in old_versions if v not in new_versions]
+    compat_vs = ['compat "%s"' % v for v in old_versions if v not in new_versions]
+    all_options = tuple(Vs + compat_vs)
+    options = (['"-compat" "%s"' % v for v in old_versions if v not in new_versions] +
+               [version_name_to_compat_name(v, ext='') for v in old_versions if v not in new_versions])
+    if len(options) > 0 or len(all_options) > 0:
+        print('To discover what files require manual updating, run:')
+        if len(options) > 0: print("git grep -- '%s' test-suite/" % r'\|'.join(options))
+        if len(all_options) > 0: print("git grep -- '%s'" % r'\|'.join(all_options))
+
+def parse_args(argv):
+    args = {
+        'assert_unchanged': False,
+        'cur_version': None,
+        'number_of_old_versions': DEFAULT_NUMBER_OF_OLD_VERSIONS
+    }
+    for arg in argv[1:]:
+        if arg == '--assert-unchanged':
+            args['assert_unchanged'] = True
+        elif arg.startswith('--cur-version='):
+            args['cur_version'] = arg[len('--cur-version='):]
+            assert(len(args['cur_version'].split('.')) == 2)
+            assert(all(map(str.isdigit, args['cur_version'].split('.'))))
+        elif arg.startswith('--number-of-old-versions='):
+            args['number_of_old_versions'] = int(arg[len('--number-of-old-versions='):])
+        else:
+            print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN]' % argv[0])
+            print('')
+            print('ERROR: Unrecognized argument: %s' % arg)
+            sys.exit(1)
+    return args
+
+if __name__ == '__main__':
+    args = parse_args(sys.argv)
+    args['cur_version'] = get_version(args['cur_version'])
+    args['number_of_compat_versions'] = args['number_of_old_versions'] + 1
+    known_versions = get_known_versions()
+    new_versions = get_new_versions(known_versions, **args)
+    assert(len(TEST_SUITE_PATHS) >= args['number_of_compat_versions'])
+    args['test_suite_paths'] = tuple(TEST_SUITE_PATHS[-args['number_of_compat_versions']:])
+    args['test_suite_descriptions'] = tuple(TEST_SUITE_DESCRIPTIONS[-args['number_of_compat_versions']:])
+    update_compat_files(known_versions, new_versions, **args)
+    update_flags(known_versions, new_versions, **args)
+    update_test_suite(new_versions, **args)
+    update_doc_index(new_versions, **args)
+    update_bug_4789(new_versions, **args)
+    update_compat_notations(known_versions, new_versions, **args)
+    display_git_grep(known_versions, new_versions)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ba0c5440..ced6ea26 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -64,8 +64,14 @@ let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
 let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
 let rawdebug = ref false
 let ppevar evk = pp (Evar.print evk)
-let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
-let ppeconstr x = pp (Termops.print_constr x)
+let pr_constr t =
+  let sigma, env = Pfedit.get_current_context () in
+  Printer.pr_constr_env env sigma t
+let pr_econstr t =
+  let sigma, env = Pfedit.get_current_context () in
+  Printer.pr_econstr_env env sigma t
+let ppconstr x = pp (pr_constr x)
+let ppeconstr x = pp (pr_econstr x)
 let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
@@ -95,9 +101,9 @@ let ppidmapgen l = pp (pridmapgen l)
 
 let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
   hov 0
-  (Termops.print_constr (EConstr.of_constr c) ++
+  (pr_constr c ++
    (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++
-    Termops.print_constr (EConstr.of_constr c) ++ str">") ++
+    pr_constr c ++ str">") ++
    (if id = id0 then mt ()
     else spc () ++ str "<canonical: " ++ Id.print id ++ str ">"))))
 
@@ -106,7 +112,7 @@ let ppididmap = ppidmap (fun _ -> Id.print)
 
 let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
   hov 1 (str"[" ++  prlist_with_sep spc Id.print l ++ str"]")
-  ++ str "," ++ spc () ++ Termops.print_constr c)
+  ++ str "," ++ spc () ++ pr_econstr c)
 
 let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
 
@@ -155,15 +161,15 @@ let ppdelta s = pp (Mod_subst.debug_pr_delta s)
 let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
 let pp_transparent_state s = pp (pr_transparent_state s)
-let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n)
-let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n)
-let pp_state_t n = pp (Reductionops.pr_state n)
+let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n)
+let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n)
+let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
 
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(Termops.pr_metaset metas)
-let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
-let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
@@ -181,7 +187,7 @@ let ppproofview p =
   pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)
@@ -203,17 +209,17 @@ let pproof p = pp(Proof.pr_proof p)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let prlev = Universes.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes
 let ppuniverse_set l = pp (LSet.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prlev l)
 let ppuniverse_context l = pp (pr_universe_context prlev l)
 let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
-let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
+let ppuniverse_opt_subst l = pp (UnivSubst.pr_universe_opt_subst l)
 let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
 let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l)
 let ppconstraints c = pp (pr_constraints Level.pr c)
-let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
+let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
@@ -221,7 +227,9 @@ let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
 let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
-  pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  pp (pr_named_context env sigma (named_context_of_val e))
 
 let ppenv e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
@@ -230,7 +238,7 @@ let ppenv e = pp
 let ppenvwithcst e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
-   str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
+   str "{" ++ Environ.fold_constants (fun a _ s -> Constant.print a ++ spc () ++ s) e (mt ()) ++ str "}")
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
@@ -299,8 +307,8 @@ let constr_display csr =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ())
 
   and sort_display = function
-    | Prop(Pos) -> "Prop(Pos)"
-    | Prop(Null) -> "Prop(Null)"
+    | Set -> "Set"
+    | Prop -> "Prop"
     | Type u -> univ_display u;
 	"Type("^(string_of_int !cnt)^")"
 
@@ -421,8 +429,8 @@ let print_pure_constr csr =
     Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u)
 
   and sort_display = function
-    | Prop(Pos) -> print_string "Set"
-    | Prop(Null) -> print_string "Prop"
+    | Set -> print_string "Set"
+    | Prop -> print_string "Prop"
     | Type u -> open_hbox();
 	print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
 
@@ -547,8 +555,8 @@ let encode_path ?loc prefix mpdir suffix id =
     | Some (mp,dir) ->
 	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
 	DirPath.repr dir) in
-  CAst.make ?loc @@ Qualid (make_qualid
-    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
+  make_qualid ?loc
+    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
 let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
@@ -567,9 +575,9 @@ let raw_string_of_ref ?loc _ = function
       encode_path ?loc "SECVAR" None [] id
 
 let short_string_of_ref ?loc _ = function
-  | VarRef id -> CAst.make ?loc @@ Ident id
-  | ConstRef cst -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (Constant.repr3 cst)))
-  | IndRef (kn,0) -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (MutInd.repr3 kn)))
+  | VarRef id -> qualid_of_ident ?loc id
+  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst)))
+  | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn)))
   | IndRef (kn,i) ->
       encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
         (Id.of_string ("_"^string_of_int i))
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index dad6dcc1..63d7d580 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -87,7 +87,7 @@ val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit
 val ppclosedglobconstridmap :
   Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit
 
-val ppglobal : Globnames.global_reference -> unit
+val ppglobal : Names.GlobRef.t -> unit
 
 val ppconst :
   Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit
@@ -139,11 +139,11 @@ val ppuniverse_instance : Univ.Instance.t -> unit
 val ppuniverse_context : Univ.UContext.t -> unit
 val ppuniverse_context_set : Univ.ContextSet.t -> unit
 val ppuniverse_subst : Univ.universe_subst -> unit
-val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit
+val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit
 val ppuniverse_level_subst : Univ.universe_level_subst -> unit
 val ppevar_universe_context : UState.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
-val ppuniverseconstraints : Universes.Constraints.t -> unit
+val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
 val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
 val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 2ddf927d..ea126e27 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,7 +1,7 @@
 open Format
 open Term
+open Constr
 open Names
-open Cbytecodes
 open Cemitcodes
 open Vmvalues
 
@@ -10,11 +10,14 @@ let ppripos (ri,pos) =
   | Reloc_annot a ->
       let sp,i = a.ci.ci_ind in
       print_string
-	("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
+        ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
-      print_string ("getglob "^(Constant.to_string kn)^"\n"));
+    print_string ("getglob "^(Constant.to_string kn)^"\n")
+  | Reloc_proj_name p ->
+    print_string ("proj "^(Projection.Repr.to_string p)^"\n")
+  );
    print_flush ()
 
 let print_vfix () = print_string "vfix"
@@ -22,8 +25,8 @@ let print_vfix_app () = print_string "vfix_app"
 let print_vswith () = print_string "switch"
 
 let ppsort = function
-  | Prop(Pos) -> print_string "Set"
-  | Prop(Null) -> print_string "Prop"
+  | Set -> print_string "Set"
+  | Prop -> print_string "Prop"
   | Type u -> print_string "Type"
author	Benjamin Barenblat <bbaren@debian.org>	2019-02-02 19:29:23 -0500
committer	Benjamin Barenblat <bbaren@debian.org>	2019-02-02 19:29:23 -0500
commit	9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
tree	bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /dev
parent	9043add656177eeac1491a73d2f3ab92bec0013c (diff)