11 files changed, 43 insertions, 10 deletions
diff --git a/doc/README.md b/doc/README.md
index b784fe92f6..ef3ccc2105 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -27,7 +27,7 @@ Dependencies
 ### HTML documentation
 
 To produce the complete documentation in HTML, you will need Coq dependencies
-listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based
+listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based
 reference manual requires Python 3, and the following Python packages:
 
   - sphinx >= 1.7.8
diff --git a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst b/doc/changelog/02-specification-language/10657-minim-toset-flex.rst
new file mode 100644
index 0000000000..8983e162fb
--- /dev/null
+++ b/doc/changelog/02-specification-language/10657-minim-toset-flex.rst
@@ -0,0 +1,3 @@
+- Changed heuristics for universe minimization to :g:`Set`: only
+  minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_,
+  by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau).
diff --git a/doc/changelog/03-notations/11276-master+fix10750.rst b/doc/changelog/03-notations/11276-master+fix10750.rst
new file mode 100644
index 0000000000..a1b8594f5f
--- /dev/null
+++ b/doc/changelog/03-notations/11276-master+fix10750.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  :cmd:`Print Visibility` was failing in the presence of only-printing notations
+  (`#11276 <https://github.com/coq/coq/pull/11276>`_,
+  by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_).
diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst
new file mode 100644
index 0000000000..2fef75dc7f
--- /dev/null
+++ b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  The tactics :tacn:`eapply`, :tacn:`refine` and its variants no
+  longer allows shelved goals to be solved by typeclass resolution.
+  (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau).
diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst
new file mode 100644
index 0000000000..cdfd2b228e
--- /dev/null
+++ b/doc/changelog/04-tactics/11203-fix-time-printing.rst
@@ -0,0 +1,4 @@
+- The optional string argument to :tacn:`time` is now properly quoted
+  under :cmd:`Print Ltac` (`#11203
+  <https://github.com/coq/coq/pull/11203>`_, fixes `#10971
+  <https://github.com/coq/coq/issues/10971>`_, by Jason Gross)
diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst
new file mode 100644
index 0000000000..ebfb6c19b1
--- /dev/null
+++ b/doc/changelog/04-tactics/11263-micromega-fix.rst
@@ -0,0 +1,6 @@
+- **Fixed**
+  Efficiency regression introduced by  PR `#9725 <https://github.com/coq/coq/pull/9725>`_.
+  (`#11263 <https://github.com/coq/coq/pull/11263>`_,
+  fixes `#11063 <https://github.com/coq/coq/issues/11063>`_,
+  and `#11242 <https://github.com/coq/coq/issues/11242>`_,
+  and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson).
diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst
new file mode 100644
index 0000000000..ecc134748d
--- /dev/null
+++ b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  ``coqtop --version`` was broken when called in the middle of an installation process
+  (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing
+  `#11254 <https://github.com/coq/coq/pull/11254>`_).
diff --git a/doc/changelog/10-standard-library/11127-trunk.rst b/doc/changelog/10-standard-library/11127-trunk.rst
new file mode 100644
index 0000000000..ef1d41d17f
--- /dev/null
+++ b/doc/changelog/10-standard-library/11127-trunk.rst
@@ -0,0 +1,2 @@
+- **Added:** theorem :g:`bezout_comm` for natural numbers
+  (`#11127 <https://github.com/coq/coq/pull/11127>`_, by Daniel de Rauglaudre).
diff --git a/doc/sphinx/dune b/doc/sphinx/dune
index 353d58c676..b788fbbeed 100644
--- a/doc/sphinx/dune
+++ b/doc/sphinx/dune
@@ -1,8 +1,10 @@
 (dirs :standard _static)
 
-(rule (targets README.gen.rst)
+(rule
+ (targets README.gen.rst)
  (deps (source_tree ../tools/coqrst) README.template.rst)
  (action (run ../tools/coqrst/regen_readme.py %{targets})))
 
-(alias (name refman-html)
-  (action (diff README.rst README.gen.rst)))
+(rule
+ (alias refman-html)
+ (action (diff README.rst README.gen.rst)))
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 81e50c0834..878118c48a 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -555,12 +555,14 @@ Applying theorems
    This tactic applies to any goal. It behaves like :tacn:`exact` with a big
    difference: the user can leave some holes (denoted by ``_``
    or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many
-   subgoals as there are holes in the term. The type of holes must be either
-   synthesized by the system or declared by an explicit cast
+   subgoals as there are remaining holes in the elaborated term. The type
+   of holes must be either synthesized by the system or declared by an explicit cast
    like ``(_ : nat -> Prop)``. Any subgoal that
    occurs in other subgoals is automatically shelved, as if calling
-   :tacn:`shelve_unifiable`. This low-level tactic can be
-   useful to advanced users.
+   :tacn:`shelve_unifiable`. The produced subgoals (shelved or not)
+   are *not* candidates for typeclass resolution, even if they have a type-class
+   type as conclusion, letting the user control when and how typeclass resolution
+   is launched on them. This low-level tactic can be useful to advanced users.
 
    .. example::
 
@@ -611,8 +613,9 @@ Applying theorems
    .. tacv:: simple notypeclasses refine @term
       :name: simple notypeclasses refine
 
-      This tactic behaves like :tacn:`simple refine` except it performs type checking
-      without resolution of typeclasses.
+      This tactic behaves like the combination of :tacn:`simple refine` and
+      :tacn:`notypeclasses refine`: it performs type checking without resolution of
+      typeclasses, does not perform beta reductions or shelve the subgoals.
 
    .. flag:: Debug Unification
 
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index a2bc90ffc0..b816ef6210 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -24,6 +24,7 @@ plugins/extraction/Extraction.v
 plugins/funind/FunInd.v
 plugins/funind/Recdef.v
 plugins/ltac/Ltac.v
+plugins/micromega/Ztac.v
 plugins/micromega/DeclConstant.v
 plugins/micromega/Env.v
 plugins/micromega/EnvRing.v