4 files changed, 33 insertions, 7 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 04b20c6889..cb6e695865 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,13 @@
 
 ### ML API
 
+Exception handling:
+
+- Coq's custom `Backtrace` module has been removed in favor of OCaml's
+  native backtrace implementation. Please use the functions in
+  `Exninfo.capture` and `iraise` when re-raising inside an exception
+  handler.
+
 Printers:
 
 - Functions such as Printer.pr_lconstr_goal_style_env have been
@@ -10,6 +17,11 @@ Printers:
   Constrextern.extern_constr which were taking a boolean argument for
   the goal style now take instead a label.
 
+Implicit arguments:
+
+- The type `Impargs.implicit_kind` was removed in favor of
+  `Glob_term.binding_kind`.
+
 ## Changes between Coq 8.10 and Coq 8.11
 
 ### ML API
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 2d187f7bae..3260040248 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -158,7 +158,7 @@ Universes
   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 released versions: V8.5-V8.10
   impacted development branches: none
   impacted coqchk versions: immune
   fixed in: PR#10664
@@ -167,6 +167,19 @@ Universes
   GH issue number: none
   risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
 
+  component: algebraic universes
+  summary: Set+2 was incorrectly simplified to Set+1
+  introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a)
+  impacted released versions: V8.10.0 V8.10.1 V8.10.2
+  impacted coqchk versions: same
+  fixed in: PR#11422
+  found by: Gilbert
+  exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration)
+  GH issue number: see PR
+  risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic
+    universes such that +2 increments do not appear), mild risk from plugins which manipulate
+    algebraic universes.
+
 Primitive projections
 
   component: primitive projections, guard condition
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index ba68501e04..2b09b2b42e 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -127,11 +127,11 @@ in time.
 - [ ] Send an e-mail on Coqdev announcing that the tag has been put so that
   package managers can start preparing package updates (including a
   `coq-bignums` compatible version).
-- [ ] Ping **@erikmd** to update the Docker images in `coqorg/coq`
+- [ ] Ping `@erikmd` to update the Docker images in `coqorg/coq`
   (requires `coq-bignums` in `extra-dev` for a beta / in `released`
   for a final release).
 - [ ] Draft a release on GitHub.
-- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and
+- [ ] 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)).
@@ -139,8 +139,6 @@ in time.
   *TODO: setup some continuous deployment for this.*
 - [ ] Merge the website update, publish the release
   and send announcement e-mails.
-- [ ] Ping **@Zimmi48** to publish a new version on Zenodo.
-  *TODO: automate this.*
 - [ ] Close the milestone
 
 ## At the final release time ##
@@ -160,7 +158,10 @@ in time.
 
 Repeat the generic process documented above for all releases.
 
+Ping `@Zimmi48` to:
+
 - [ ] Switch the default version of the reference manual on the website.
+- [ ] Publish a new version on Zenodo.
 
 ## At the patch-level release time ##
 
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index f0b8d6630f..fca7b77fc2 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -1,11 +1,11 @@
 # Coq XML Protocol
 
 This document is based on documentation originally written by CJ Bell
-for his [vscoq](https://github.com/siegebell/vscoq/) project.
+for his [vscoq](https://github.com/coq-community/vscoq/) project.
 
 Here, the aim is to provide a "hands on" description of the XML
 protocol that coqtop and IDEs use to communicate. The protocol first appeared 
-with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/siegebell/vscoq/), and other user interfaces.
+with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces.
 
 A somewhat out-of-date description of the async state machine is
 [documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md).