14 files changed, 107 insertions, 23 deletions
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
index 919e2a735f..16c4ac37d9 100644
--- a/dev/ci/docker/README.md
+++ b/dev/ci/docker/README.md
@@ -4,10 +4,33 @@ 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.
+The Gitlab CI will build a docker image unless the CI environment variable
+`SKIP_DOCKER` is set to `true`. This image will be
+stored in the [Gitlab container registry](https://gitlab.com/coq/coq/container_registry)
+under the name given by the `CACHEKEY` variable from
+the [Gitlab CI configuration file](../../../.gitlab-ci.yml).
+
+In Coq's default CI, `SKIP_DOCKER` is set so as to avoid running a lengthy redundant job.
+
+It can be used to regenerate a fresh Docker image on Gitlab through the following steps.
+- Change the `CACHEKEY` variable to a fresh name in the CI configuration in a new commit.
+- Push this commit to a Github PR. This will trigger a Gitlab CI run that will
+  immediately fail, as the Docker image is missing and the `SKIP_DOCKER`
+  default value prevents rebuilding the image.
+- Run a new pipeline on Gitlab with that PR branch, using the green "Run pipeline"
+  button on the [web interface](https://gitlab.com/coq/coq/pipelines),
+  with the `SKIP_DOCKER` environment variable set to `false`. This will run a `docker-boot` process, and
+  once completed, a new Docker image will be available in the container registry,
+  with the name set in `CACHEKEY`.
+- Any pipeline with the same `CACHEKEY` will now automatically reuse that
+  image without rebuilding it from scratch.
+
+For documentation purposes, we also require keeping in sync the `CACHEKEY` comment
+from the first line of the [Dockerfile](bionic_coq/Dockerfile) in the same
+commit.
+
+In case you do not have the rights to run Gitlab CI pipelines, you should ask
+the ci-maintainers Github team to do it for you.
 
 ## Manual Building
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index edca83c6ef..1cad46cd89 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-09-20-V01"
+# CACHEKEY: "bionic_coq-V2019-11-05-V01"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -39,7 +39,7 @@ ENV COMPILER="4.05.0"
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.7.0"
+    BASE_ONLY_OPAM="elpi.1.8.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6"
diff --git a/dev/ci/user-overlays/09867-primitive-floats.sh b/dev/ci/user-overlays/09867-primitive-floats.sh
new file mode 100644
index 0000000000..a0e9085afd
--- /dev/null
+++ b/dev/ci/user-overlays/09867-primitive-floats.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9867" ] || [ "$CI_BRANCH" = "primitive-floats" ]; then
+
+    unicoq_CI_REF=primitive-floats
+    unicoq_CI_GITURL=https://github.com/validsdp/unicoq
+
+    elpi_CI_REF=primitive-floats
+    elpi_CI_GITURL=https://github.com/validsdp/coq-elpi
+
+    coqhammer_CI_REF=primitive-floats
+    coqhammer_CI_GITURL=https://github.com/validsdp/coqhammer
+
+fi
diff --git a/dev/ci/user-overlays/10358-gares-elpi13.sh b/dev/ci/user-overlays/10358-gares-elpi13.sh
deleted file mode 100644
index d2ba9b5ddf..0000000000
--- a/dev/ci/user-overlays/10358-gares-elpi13.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10358" ] || [ "$CI_BRANCH" = "elpi-13-coq" ]; then
-
-    elpi_CI_REF="elpi-13-coq"
-    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh
new file mode 100644
index 0000000000..f4840c2a83
--- /dev/null
+++ b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10681" ] || [ "$CI_BRANCH" = "proof+private_entry" ]; then
+
+    equations_CI_REF=proof+private_entry
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/10738-gares-elpi1.7.sh b/dev/ci/user-overlays/10738-gares-elpi1.7.sh
deleted file mode 100644
index 8922badf90..0000000000
--- a/dev/ci/user-overlays/10738-gares-elpi1.7.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10738" ] || [ "$CI_BRANCH" = "elpi1.7" ]; then
-
-    elpi_CI_REF="coq-master+elpi1.7"
-    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh b/dev/ci/user-overlays/11051-gares-elpi-1.8.sh
new file mode 100644
index 0000000000..7845654375
--- /dev/null
+++ b/dev/ci/user-overlays/11051-gares-elpi-1.8.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11051" ] || [ "$CI_BRANCH" = "elpi-1.8" ]; then
+
+    elpi_CI_REF="coq-master+v1.2"
+    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ab9df12766..8ab00c6fd8 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,8 @@
 
 ### ML API
 
+- Function UnivGen.global_of_constr has been removed.
+
 - Functions and types deprecated in 8.10 have been removed in Coq
   8.11.
 
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 6d90ced12d..0631b3ad59 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -112,8 +112,8 @@ Universes
   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
+  impacted coqchk versions: V8.5 to V8.9
+  fixed in: ec4aa4971f (58e1d0f200 for the checker)
   found by: Gaëtan Gilbert
   exploit: test-suite/misc/poly-capture-global-univs
   GH issue number: #8341
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 845680d7e3..0fc0a413ba 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -45,6 +45,7 @@ Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/de
   - [File Loaded](#feedback-fileloaded)
   - [Message](#feedback-message)
   - [Custom](#feedback-custom)
+* [Highlighting Text](#highlighting)
 
 Sentences: each command sent to Coqtop is a "sentence"; they are typically terminated by ".\s" (followed by whitespace or EOF).
 Examples: "Lemma a: True.", "(* asdf *) Qed.", "auto; reflexivity."
@@ -753,3 +754,43 @@ Ex: `status = "Idle"` or `status = "proof: myLemmaName"` or `status = "Dead"`
 </feedback>
 ```
 
+## <a name="highlighting">Highlighting Text</a>
+
+[Proof diffs](https://coq.inria.fr/distrib/current/refman/proof-engine/proof-handling.html#showing-differences-between-proof-steps)
+highlight differences between the current and previous proof states in the displayed output.
+These are represented by tags embedded in output fields of the XML document.
+
+There are 4 tags that indicate how the enclosed text should be highlighted:
+- diff.added - added text
+- diff.removed - removed text
+- diff.added.bg - unchanged text in a line that has additions ("bg" for "background")
+- diff.removed.bg - unchanged text in a line that has removals
+
+CoqIDE, Proof General and coqtop currently use 2 shades of green and 2 shades of red
+as the background color for highlights.  Coqtop and CoqIDE also apply underlining and/or
+strikeout highlighting for the sake of the color blind.
+
+For example, `<diff.added>ABC</diff.added>` indicates that "ABC" should be highlighted
+as added text.  Tags can be nested, such as:
+`<diff.added.bg>A <diff.added> + 1</diff.added> + B</diff.added.bg>`.  IDE code
+displaying highlighted strings should maintain a stack for nested tags and the associated
+highlight.  Currently the diff code only nests at most 2 tags deep.
+If an IDE uses other highlights such as text foreground color or italic text, it may
+need to merge the background color with those other highlights to give the desired
+(IDE dependent) behavior.
+
+The current implementations avoid highlighting white space at the beginning or the
+end of a line.  This gives a better appearance.
+
+There may be additional text that is marked with other tags in the output text.  IDEs probably
+should ignore and not display tags they don't recognize.
+
+Some internal details about generating tags within Coq (e.g. if you want to add
+additional tags):
+
+Tagged output strings are generated from Pp.t's.  Use Pp.tag to highlight a Pp.t using
+one of the tags listed above.  A span of tokens can be marked by using "start.<tag>" on
+the first token and "end.<tag>" on the last token.  (Span markers are needed because a span of
+tokens in the output may not match nesting of layout boxes in the Pp.t.)
+The conversion from the Pp.t to the XML-tagged string replaces the "start.\*" and "end.\*"
+tags with the basic tags.
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index 8736c0f9b8..e7a0ba4f6c 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/31c38894c90429c9554eab1b416e59e3b6e054df.tar.gz";
-  sha256 = "1fv14rj5zslzm14ak4lvwqix94gm18h28376h4hsmrqqpnfqwsdw";
+  url = "https://github.com/NixOS/nixpkgs/archive/4cd2cb43fb3a87f48c1e10bb65aee99d8f24cb9d.tar.gz";
+  sha256 = "1d6rmq67kdg5gmk94wx2774qw89nvbhy6g1f2lms3c9ph37hways";
 })
diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index ea96de970a..ec59a6047f 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -7,7 +7,8 @@ echo "Where? (type a prefix)"
 (cd doc/changelog && ls -d */)
 read -r where
 
-where=$(echo doc/changelog/"$where"*)
+where="doc/changelog/$where"
+if ! [ -d "$where" ]; then where=$(echo "$where"*); fi
 where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst"
 
 # shellcheck disable=SC2016
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index aa28bce018..ccb8658eee 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -307,6 +307,8 @@ let constr_display csr =
       ^(array_display bl)^")"
   | Int i ->
       "Int("^(Uint63.to_string i)^")"
+  | Float f ->
+      "Float("^(Float64.to_string f)^")"
 
   and array_display v =
     "[|"^
@@ -439,6 +441,8 @@ let print_pure_constr csr =
       in print_string"{"; print_fix (); print_string"}"
   | Int i ->
      print_string ("Int("^(Uint63.to_string i)^")")
+  | Float f ->
+      print_string ("Float("^(Float64.to_string f)^")")
 
   and box_display c = open_hovbox 1; term_display c; close_box()
 
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 863d930968..11565b99eb 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -84,6 +84,7 @@ and ppwhd whd =
   | Vconstr_const i -> print_string "C(";print_int i;print_string")"
   | Vconstr_block b -> ppvblock b
   | Vint64 i -> printf "int64(%LiL)" i
+  | Vfloat64 f -> printf "float64(%.17g)" f
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s