17 files changed, 353 insertions, 52 deletions
diff --git a/dev/base_include b/dev/base_include
index fc38305cc..6f54ecb24 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -108,8 +108,6 @@ open Inductiveops
 open Locusops
 open Find_subterm
 open Unification
-open Miscops
-open Miscops
 open Nativenorm
 open Typeclasses
 open Typeclasses_errors
@@ -231,7 +229,7 @@ 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 ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
diff --git a/dev/ci/README.md b/dev/ci/README.md
index dc586c61f..45176581c 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -47,16 +47,13 @@ CI.
 
 ### Add your development by submitting a pull request
 
-Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at
-[`ci-coq-dpdgraph.sh`](/dev/ci/ci-coq-dpdgraph.sh) or
-[`ci-fiat-parsers.sh`](/dev/ci/ci-fiat-parsers.sh) for simple examples);
-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
-[`.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.**
+Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding
+variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the
+corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to
+[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run.
+Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an
+example. **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
@@ -83,17 +80,12 @@ We are currently running tests on the following platforms:
 
 - 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
+  [pre-commit hook](../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.
 
-GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit
-message to bypass CI. Do not use this unless your commit only changes files
-that are not compiled (e.g. Markdown files like this one, or files under
-[`.github/`](/.github/)).
-
 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:
 
@@ -112,7 +104,7 @@ there are some.
 
 You can also run one CI target locally (using `make ci-somedev`).
 
-See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
+See also [`test-suite/README.md`](../../test-suite/README.md) for information about adding new tests to the test-suite.
 
 ### Breaking changes
 
@@ -123,7 +115,7 @@ patch (or ask someone to prepare a patch) to fix the project:
    the project to your changes.
 2. Test your pull request with your adapted version of the external project by
    adding an overlay file to your pull request (cf.
-   [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)).
+   [`dev/ci/user-overlays/README.md`](user-overlays/README.md)).
 3. Fixes to external libraries (pure Coq projects) *must* be backward
    compatible (i.e. they should also work with the development version of Coq,
    and the latest stable version). This will allow you to open a PR on the
@@ -137,7 +129,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`](../../CHANGES) file.
 
 Advanced GitLab CI information
 ------------------------------
@@ -173,8 +165,9 @@ automatically built and uploaded to your GitLab registry, and is
 loaded by subsequent jobs.
 
 **IMPORTANT**: When updating Coq's CI docker image, you must modify
-the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`,
-and `Dockerfile`.
+the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml),
+[`.circleci/config.yml`](../../.circleci/config.yml),
+and [`Dockerfile`](docker/bionic_coq/Dockerfile)
 
 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
@@ -182,4 +175,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/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 87d837b38..3807ff90c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -119,7 +119,7 @@
 ########################################################################
 # coq-dpdgraph
 ########################################################################
-: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}"
+: "${coq_dpdgraph_CI_BRANCH:=coq-master}"
 : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}"
 
 ########################################################################
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 5b5cbd11a..85df249d3 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -93,17 +93,26 @@ install_ssreflect()
   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 && \
-    sed -i.bak '/all\/all.v/d'  Make && \
-    sed -i.bak '/character/d'   Make && \
-    sed -i.bak '/real_closed/d' Make && \
-    sed -i.bak '/solvable/d'    Make && \
-    sed -i.bak '/field/d'       Make && \
-    sed -i.bak '/fingroup/d'    Make && \
-    sed -i.bak '/algebra/d'     Make && \
-    make Makefile.coq && make -f Makefile.coq all && make install )
+    make Makefile.coq && \
+    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'
+
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
+  ( cd "${mathcomp_CI_DIR}/mathcomp" && \
+    make Makefile.coq && \
+    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-geocoq.sh b/dev/ci/ci-geocoq.sh
index 920272bcf..24cd9c427 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,4 +7,6 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
 
 git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
 
+install_ssralg
+
 ( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 1a83593f5..52f851917 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-06-04-V2"
+# CACHEKEY: "bionic_coq-V2018-06-13-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -27,7 +27,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.
 # `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 jbuilder.1.0+beta20 ounit.2.0.8" \
-    CI_OPAM="menhir.20180530 elpi.1.0.3 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV CAMLP5_VER="6.14" \
diff --git a/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh b/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh
new file mode 100644
index 000000000..9d96b6d4c
--- /dev/null
+++ b/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh
@@ -0,0 +1,4 @@
+ if [ "$CI_PULL_REQUEST" = "664" ] || [ "$CI_BRANCH" = "trunk+fix-5500-too-weak-test-return-clause" ]; then
+    fiat_parsers_CI_BRANCH=master+change-for-coq-pr664-compatibility
+    fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat
+fi
diff --git a/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh
new file mode 100644
index 000000000..b4f716139
--- /dev/null
+++ b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh
@@ -0,0 +1,8 @@
+_OVERLAY_BRANCH=misctypes+bye2
+
+if [ "$CI_PULL_REQUEST" = "7677" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/07797-rm-reference.sh b/dev/ci/user-overlays/07797-rm-reference.sh
new file mode 100644
index 000000000..f7811cd6f
--- /dev/null
+++ b/dev/ci/user-overlays/07797-rm-reference.sh
@@ -0,0 +1,20 @@
+_OVERLAY_BRANCH=rm-reference
+
+if [ "$CI_PULL_REQUEST" = "7797" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations.git
+
+    ltac2_CI_BRANCH="fix-7797"
+    ltac2_CI_GITURL=https://github.com/ppedrot/Ltac2.git
+
+    quickchick_CI_BRANCH="$_OVERLAY_BRANCH"
+    quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick.git
+
+    coq_dpdgraph_CI_BRANCH="$_OVERLAY_BRANCH"
+    coq_dpdgraph_CI_GITURL=https://github.com/maximedenes/coq-dpdgraph.git
+
+    Elpi_CI_BRANCH="$_OVERLAY_BRANCH"
+    Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi.git
+
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index aec2dfe0a..41212568d 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -6,7 +6,7 @@ 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
-[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh):
+[`ci-basic-overlay.sh`](../ci-basic-overlay.sh):
 give the name of your branch using a `_CI_BRANCH` variable and the location of
 your fork using a `_CI_GITURL` variable.
 
@@ -28,4 +28,4 @@ if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
 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/doc/MERGING.md b/dev/doc/MERGING.md
index 65457b63a..c0cd9c8cd 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -6,7 +6,7 @@ This document describes how patches, submitted as pull requests (PRs) on the
 
 ## Code owners
 
-The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
+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.
 
@@ -51,10 +51,10 @@ say in a comment they think a review is not required and proceed with the merge.
 
 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](/dev/ci/README.md#Breaking-changes) and the PR can be tested
-with these fixes thanks to ["overlays"](/dev/ci/user-overlays/README.md).
+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`](/CHANGES) file.
+Moreover the PR must absolutely update the [`CHANGES`](../../CHANGES) 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.
@@ -74,7 +74,17 @@ 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](/dev/tools/merge-pr.sh).
+[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
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index bb8189efc..f3fc126f9 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,14 @@
 
 ### 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`
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
new file mode 100644
index 000000000..293b01f63
--- /dev/null
+++ b/dev/doc/critical-bugs
@@ -0,0 +1,226 @@
+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: ?
+
+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
+
+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: "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/profiling.txt b/dev/doc/profiling.txt
index 9d2ebf0d4..b5dd8445d 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux.
 
 In Coq source folder:
 
-opam switch 4.02.1+fp
+opam switch 4.02.3+fp
 ./configure -local -debug
 make
 perf record -g bin/coqtop -compile file.v
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 00d04e6b3..320ef6ed0 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -140,6 +140,24 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then
     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")
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 10a7a4158..844ad9188 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -549,8 +549,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 ->
@@ -569,9 +569,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/vm_printers.ml b/dev/vm_printers.ml
index 16917586f..7589e5348 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -15,7 +15,10 @@ let ppripos (ri,pos) =
   | 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 "^(Constant.to_string p)^"\n")
+  );
    print_flush ()
 
 let print_vfix () = print_string "vfix"