7 files changed, 124 insertions, 23 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 372e40a0b7..37c6e2f619 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -52,7 +52,7 @@ order to use them, do:
 
 ```
 $ make -f Makefile.dune voboot                # Only once per session
-$ dune exec dev/shim/coqtop-prelude
+$ dune exec -- dev/shim/coqtop-prelude
 ```
 
 or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets
@@ -108,14 +108,14 @@ automatically.
 You can use `ocamldebug` with Dune; after a build, do:
 
 ```
-dune exec dev/dune-dbg /path/to/foo.v
+dune exec -- dev/dune-dbg /path/to/foo.v
 (ocd) source dune_db
 ```
 
 or
 
 ```
-dune exec dev/dune-dbg checker Foo
+dune exec -- dev/dune-dbg checker Foo
 (ocd) source dune_db
 ```
 
@@ -130,7 +130,7 @@ For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`.
 
 After doing `make -f Makefile.dune voboot`, the following commands should work:
 ```
-dune exec dev/shim/coqbyte-prelude
+dune exec -- dev/shim/coqbyte-prelude
 > Drop.
 # #directory "dev";;
 # #use "include_dune";;
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index a14781a058..b8987b7086 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -89,7 +89,7 @@ enables partial recalculation of dependencies (only the dependencies
 of changed files are recomputed).
 
 If you add a dependency to a Coq camlp5 extension (grammar.cma or
-q_constr.cmo), then see sections ".ml4 files" and "new files".
+q_constr.cmo), then see sections ".mlg files" and "new files".
 
 Cleaning Targets
 ----------------
@@ -113,13 +113,13 @@ Targets for cleaning various parts:
 
  - docclean: clean documentation
 
-.ml4/.mlp files
+.mlg/.mlp files
 ---------------
 
 There is now two kinds of preprocessed files : 
  - a .mlp do not need grammar.cma (they are in grammar/)
- - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
-   except coqide_main.ml4 and its specific rule
+ - a .mlg is now always preprocessed with grammar.cma (and q_constr.cmo),
+   except coqide_main.mlg and its specific rule
 
 This classification replaces the old mechanism of declaring the use
 of a grammar extension via a line of the form:
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/coq-src-description.txt b/dev/doc/coq-src-description.txt
index e5e4f740bd..096ffe6a1c 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -20,7 +20,7 @@ Special components
 grammar :
 
  Camlp5 syntax extensions. The file grammar/grammar.cma is used
- to pre-process .ml4 files containing EXTEND constructions,
+ to pre-process .mlg files containing EXTEND constructions,
  either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND.
  This grammar.cma incorporates many files from other directories
  (mainly parsing/), plus some specific files in grammar/.
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 01c2b574a2..6d90ced12d 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -119,6 +119,28 @@ Universes
   GH issue number: #8341
   risk: unlikely to be activated by chance (requires a plugin)
 
+  component: template polymorphism
+  summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though)
+  impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found
+  impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit)
+  fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau)
+  found by: Gilbert using explicit sharing of universes, exploit found for 8.5-8.9 by Pédrot, other variants generating sharing using sections, or using ltac tricks by Sozeau, exploit in 8.4 by Herbelin and Jason Gross by adding new tricks to Sozeau's variants
+  exploit: test-suite/failure/Template.v
+  GH issue number: #9294
+  risk: moderate risk to be activated by chance
+
+  component: universe polymorphism, asynchronous proofs
+  summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
+  introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
+  impacted released: V8.5-V8.10
+  impacted development branches: none
+  impacted coqchk versions: immune
+  fixed in: PR#10664
+  found by: Pédrot
+  exploit: no test
+  GH issue number: none
+  risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
+
 Primitive projections
 
   component: primitive projections, guard condition
@@ -228,6 +250,17 @@ Conversion machines
   exploit: test-suite/bugs/closed/bug_9684.v
   GH issue number: #9684
 
+  component: lazy machine
+  summary: incorrect De Bruijn handling when inferring the relevance mark for a lambda
+  introduced: 2019-03-15, 23f84f37c674a07e925925b7e0d50d7ee8414093 and 71b9ad8526155020c8451dd326a52e391a9a8585, SkySkimmer
+  impacted released versions: 8.10.0
+  impacted coqchk versions: 8.10.0
+  found by: ppedrot investigating unexpected conversion failures with SProp
+  exploit: test-suite/bugs/closed/bug_10904.v
+  GH issue number: #10904
+  risk: none without using -allow-sprop (off by default in 8.10.0),
+        otherwise could be exploited by mistake
+
 Conflicts with axioms in library
 
   component: library of real numbers
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 452160ea5a..1c486b024d 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -2,6 +2,11 @@
 
 ## As soon as the previous version branched off master ##
 
+In principle, these steps should be undertaken by the RM of the next
+release. Unfortunately, we have not yet been able to nominate RMs
+early enough in the process for this person to be known at that point
+in time.
+
 - [ ] 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
@@ -54,25 +59,39 @@
 - [ ] 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).
+
+  The command that was used in the previous versions to get the list
+  of contributors for this version is `git shortlog -s -n
+  VX.X+alpha..master | cut -f2 | sort -k 2`. Note that the ordering is
+  approximative as it will misplace people with middle names. It is
+  also probably not correctly handling `Co-authored-by` info that we
+  have been using more lately, so should probably be updated to
+  account for this.
 
 ## On the date of the feature freeze ##
 
 - [ ] Create the new version branch `vX.X` (using this name will ensure that
   the branch will be automatically protected).
+- [ ] Pin the versions of libraries and plugins in
+  `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it
+  exists, a branch dedicated to compatibility with the corresponding
+  Coq branch).
 - [ ] 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.
+- [ ] Start a new project to track PR backporting. The project should
+  have a "Request X.X+beta1 inclusion" column for the PRs that were
+  merged in `master` that are to be considered for backporting, and a
+  "Shipped in X.X+beta1" columns to put what was backported. A message
+  to **@coqbot** in the milestone description tells it to
+  automatically add merged PRs to the "Request ... inclusion" column
+  and backported PRs to the "Shipped in ..." column. See previous
+  milestones for examples. When moving to the next milestone
+  (e.g. X.X.0), you can clear and remove the "Request X.X+beta1
+  inclusion" column and create new "Request X.X.0 inclusion" and
+  "Shipped in X.X.0" columns.
+
+  The release manager is the person responsible for merging PRs that
+  target the version branch and backporting appropriate PRs that are
+  merged into `master`.
 - [ ] 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.
@@ -80,6 +99,11 @@
 ## Before the beta release date ##
 
 - [ ] Ensure the Credits chapter has been updated.
+- [ ] Prepare the release notes (see e.g.,
+  [#10833](https://github.com/coq/coq/pull/10833)): in a PR against the `master`
+  branch, move the contents from all files of `doc/changelog/` that appear in
+  the release branch into the manual `doc/sphinx/changes.rst`. Merge that PR
+  into the `master` branch and backport it to the version branch.
 - [ ] 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
@@ -120,6 +144,7 @@
 
 ## At the final release time ##
 
+- [ ] Prepare the release notes (see above)
 - [ ] In a PR:
   - Change the version name from X.X.0 and the magic numbers (see
   [#7271](https://github.com/coq/coq/pull/7271/files)).
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index a3e1a4e90b..0fc0a413ba 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -9,7 +9,7 @@ with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming
 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).
+[documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md).
 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.md`](/dev/doc/changes.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.