21 files changed, 390 insertions, 69 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index f4ec218b6..3608f7305 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -970,6 +970,10 @@ function make_lablgtk {
     # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch
 
     log2 make world
+
+    # lablgtk does not escape FINDLIBDIR path, which can contain backslashes
+    sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make
+
     log2 make install
     log2 make clean
     build_post
diff --git a/dev/ci/README.md b/dev/ci/README.md
index bb13587e9..dee3d2aff 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -36,9 +36,8 @@ On the condition that:
 - You do not push, to the branches that we test, commits that haven't been
   first tested to compile with the corresponding branch(es) of Coq.
 
-- Your development compiles in less than 35 minutes with just two threads.
-  If this is not the case, consider adding a "lite" target that compiles just
-  part of it.
+- You maintain a reasonable build time for your development, or you provide
+  a "lite" target that we can use.
 
 In case you forget to comply with these last three conditions, we would reach
 out to you and give you a 30-day grace period during which your development
@@ -54,9 +53,10 @@ Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at
 set the corresponding variables in
 [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding
 target to [`Makefile.ci`](/Makefile.ci); add new jobs to
-[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that
-this new target is run. **Do not hesitate to submit an incomplete pull request
-if you need help to finish it.**
+[`.gitlab-ci.yml`](/.gitlab-ci.yml),
+[`.circleci/config.yml`](/.circleci/config.yml) and
+[`.travis.yml`](/.travis.yml) so that this new target is run. **Do not
+hesitate to submit an incomplete pull request if you need help to finish it.**
 
 You may also be interested in having your development tested in our
 performance benchmark. Currently this is done by providing an OPAM package
@@ -71,24 +71,39 @@ When you submit a pull request (PR) on Coq GitHub repository, this will
 automatically launch a battery of CI tests. The PR will not be integrated
 unless these tests pass.
 
-Currently, we have two CI platforms:
+We are currently running tests on the following platforms:
 
-- Travis is the main CI platform. It tests the compilation of Coq, of the
+- GitLab CI is the main CI platform. It tests the compilation of Coq, of the
   documentation, and of CoqIDE on Linux with several versions of OCaml /
   camlp5, and with warnings as errors; it runs the test-suite and tests the
-  compilation of several external developments. It also tests the compilation
-  of Coq on OS X.
+  compilation of several external developments.
+
+- Circle CI runs tests that are redundant with GitLab CI and may be removed
+  eventually.
+
+- Travis CI is used to test the compilation of Coq and run the test-suite on
+  macOS. It also runs a linter that checks whitespace discipline. A
+  [pre-commit hook](/dev/tools/pre-commit) is automatically installed by
+  `./configure`. It should allow complying with this discipline without pain.
 
 - AppVeyor is used to test the compilation of Coq and run the test-suite on
   Windows.
 
-You can anticipate the results of these tests prior to submitting your PR
-by having them run of your fork of Coq, on GitHub or GitLab. This can be
-especially helpful given that our Travis platform is often overloaded and
-therefore there can be a significant delay before these tests are actually
-run on your PR. To take advantage of this, simply create a Travis account
-and link it to your GitHub account, or activate the pipelines on your GitLab
-fork.
+You can anticipate the results of most of these tests prior to submitting your
+PR by running GitLab CI on your private branches. To do so follow these steps:
+
+1. Log into GitLab CI (the easiest way is to sign in with your GitHub account).
+2. Click on "New Project".
+3. Choose "CI / CD for external repository" then click on "GitHub".
+4. Find your fork of the Coq repository and click on "Connect".
+5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project).
+6. You are encouraged to go to the CI / CD general settings and increase the
+   timeout from 1h to 2h for better reliability.
+
+Now everytime you push (including force-push unless you changed the default
+GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and
+CI will be run. You will receive an e-mail with a report of the failures if
+there are some.
 
 You can also run one CI target locally (using `make ci-somedev`).
 
@@ -97,36 +112,53 @@ so that it doesn't, or provide a branch fixing these developments (or at
 least work with the author of the development / other Coq developers to
 prepare these fixes). Then, add an overlay in
 [`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there)
-in a separate commit in your PR.
+as part of your PR.
 
 The process to merge your PR is then to submit PRs to the external
 development repositories, merge the latter first (if the fixes are
-backward-compatible), drop the overlay commit and merge the PR on Coq then.
+backward-compatible), and merge the PR on Coq then.
 
 See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
 
 
-Travis specific information
----------------------------
+Advanced GitLab CI information
+------------------------------
 
-Travis rebuilds all of Coq's executables and stdlib for each job. Coq
-is built with `./configure -local`, then used for the job's test.
-
-
-GitLab specific information
----------------------------
-
-GitLab is set up to use the "build artifact" feature to avoid
-rebuilding Coq. In one job, Coq is built with `./configure -prefix
-install` and `make install` is run, then the `install` directory
+GitLab CI is set up to use the "build artifact" feature to avoid
+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, in two different copies varying in the OCaml
-  version used to build Coq
+  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.
 
 As an exception to the above, jobs testing that compilation triggers
-no Ocaml warnings build Coq in parallel with other tests.
+no OCaml warnings build Coq in parallel with other tests.
+
+### GitLab and Windows
+
+
+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).
+
+The Windows jobs are enabled on Coq's repository, where pipelines for
+pull requests run.
+
+### GitLab and Docker
+
+System and opam packages are installed in a Docker image. The image is
+automatically built and uploaded to your GitLab registry, and is
+loaded by subsequent jobs.
+
+The Docker building job reuses the uploaded image if it is available,
+but if you wish to save more time you can skip the job by setting
+`SKIP_DOCKER` to `true`.
+
+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.
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 93e7bd99a..c72705c7f 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -5,5 +5,5 @@ tar -xf opam64.tar.xz
 bash opam64/install.sh
 opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
 eval "$(opam config env)"
-opam install -y ocamlfind camlp5
+opam install -y 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 1ae2ad0ac..5c882ee85 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -11,6 +11,8 @@
 ########################################################################
 : "${mathcomp_CI_BRANCH:=master}"
 : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}"
+: "${oddorder_CI_BRANCH:=master}"
+: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}"
 
 ########################################################################
 # UniMath
@@ -91,6 +93,12 @@
 : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}"
 
 ########################################################################
+# cross-crypto
+########################################################################
+: "${cross_crypto_CI_BRANCH:=master}"
+: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}"
+
+########################################################################
 # fiat_parsers
 ########################################################################
 : "${fiat_parsers_CI_BRANCH:=master}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 189734a0b..f867fd189 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -10,6 +10,10 @@ if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
+    if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
+    then
+        export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+    fi
 else
     if [ -n "${TRAVIS}" ];
     then
@@ -67,11 +71,6 @@ git_checkout()
     echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
 }
 
-checkout_mathcomp()
-{
-  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}"
-}
-
 make()
 {
     # +x: add x only if defined
@@ -89,7 +88,8 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp "${mathcomp_CI_DIR}"
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
   ( cd "${mathcomp_CI_DIR}/mathcomp" && \
     sed -i.bak '/ssrtest/d'     Make && \
     sed -i.bak '/odd_order/d'   Make && \
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh
new file mode 100755
index 000000000..a0d3aa655
--- /dev/null
+++ b/dev/ci/ci-cross-crypto.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto"
+
+git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}"
+( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive )
+
+( cd "${cross_crypto_CI_DIR}" && make )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 845addb4c..5d96c2499 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -6,6 +6,8 @@ ci_dir="$(dirname "$0")"
 fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto"
 
 git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}"
+
 ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
 
-( cd "${fiat_crypto_CI_DIR}" && make lite lite-display )
+fiat_crypto_CI_TARGETS="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index bd1d88993..920272bcf 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,6 +7,4 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
 
 git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
 
-( cd "${GeoCoq_CI_DIR}"                                     && \
-  ./configure-ci.sh                                       && \
-  make )
+( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 8c6b910bb..20328baf2 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -5,11 +5,10 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
+oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order"
 
-checkout_mathcomp "${mathcomp_CI_DIR}"
+git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}"
 
-# odd_order takes too much time for travis.
-( cd "${mathcomp_CI_DIR}/mathcomp"                  && \
-  sed -i.bak '/PFsection/d'                  Make && \
-  sed -i.bak '/stripped_odd_order_theorem/d' Make && \
-  make Makefile.coq && make -f Makefile.coq all )
+( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install )
+( cd "${oddorder_CI_DIR}/" && make )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 62a949f59..aa20fe1ff 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -7,7 +7,4 @@ UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath"
 
 git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}"
 
-( cd "${UniMath_CI_DIR}"                        && \
-  sed -i.bak '/Folds/d'              Makefile && \
-  sed -i.bak '/HomologicalAlgebra/d' Makefile && \
-  make BUILD_COQ=no )
+( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 79001c547..7a097eaab 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -5,9 +5,6 @@ ci_dir="$(dirname "$0")"
 
 VST_CI_DIR="${CI_BUILD_DIR}/VST"
 
-# opam install -j ${NJOBS} -y menhir
 git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}"
 
-# We have to omit progs as otherwise we timeout on Travis; on Gitlab
-# we will be able to just use `make`
-( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs )
+( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 920100157..689d203a1 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -43,4 +43,4 @@ RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \
 
 # BE+flambda switch
 RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE $CI_OPAM
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
index 6daf337a7..307680aa5 100755
--- a/dev/ci/docker/bionic_coq/hooks/post_push
+++ b/dev/ci/docker/bionic_coq/hooks/post_push
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 
-COQCI_VERSION=V2018-05-07
+COQCI_VERSION=V2018-05-07-V2
 docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION
 docker push $DOCKER_REPO:$COQCI_VERSION
 
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
new file mode 100644
index 000000000..70278e6d0
--- /dev/null
+++ b/dev/ci/gitlab.bat
@@ -0,0 +1,50 @@
+@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+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
+)
+
+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 DESTCOQ=C:\coq%ARCH%_inst
+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 -make=N ^
+  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
+7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+
+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
+  )
+)
+
+GOTO :EOF
+
+:ErrorExit
+  ECHO ERROR %0 failed
+  EXIT /b 1
diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
new file mode 100644
index 000000000..517088a24
--- /dev/null
+++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then
+
+    ltac2_CI_BRANCH=fast-constr-match-no-context
+    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 84ff94c66..a466124c1 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -109,9 +109,8 @@ There are two cases to consider:
 
 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 tutorial to
-creating your own GPG key:
-<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/>
+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.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index e9faa61c0..ff448abe8 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -28,6 +28,11 @@ Proof engine
   should indicate what the canonical form is. An important change is
   the move of `Globnames.global_reference` to `Names.GlobRef.t`.
 
+### 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.
+
 ## Changes between Coq 8.7 and Coq 8.8
 
 ### Bug tracker
diff --git a/dev/tools/check-owners-pr.sh b/dev/tools/check-owners-pr.sh
new file mode 100755
index 000000000..d2910279b
--- /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 000000000..1a97508ab
--- /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 62fdaec80..70a9756e5 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
@@ -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/pre-commit b/dev/tools/pre-commit
index b56925c37..ad2f2f93e 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -14,9 +14,9 @@ then
 
     # We fix whitespace in the index and in the working tree
     # separately to preserve non-added changes.
-    index=$(mktemp "git-fix-ws-index.XXXXX")
-    fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXX")
-    tree=$(mktemp "git-fix-ws-tree.XXXXX")
+    index=$(mktemp "git-fix-ws-index.XXXXXX")
+    fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX")
+    tree=$(mktemp "git-fix-ws-tree.XXXXXX")
     1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'."
     1>&2 echo "If an error destroys your changes you can recover using them."
     1>&2 echo "(The files are cleaned up on success.)"