14 files changed, 90 insertions, 13 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/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst
new file mode 100644
index 0000000000..ae9888512d
--- /dev/null
+++ b/doc/changelog/03-notations/11311-custom-entries-recursive.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Recursive notations with custom entries were incorrectly parsing `constr`
+  instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_
+  by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_,
+  `#9490 <https://github.com/coq/coq/pull/9490>`_).
diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst
new file mode 100644
index 0000000000..2815f8af8a
--- /dev/null
+++ b/doc/changelog/04-tactics/10760-more-rapply.rst
@@ -0,0 +1,7 @@
+- The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles
+  arbitrary numbers of underscores and takes in a :g:`uconstr`.  In
+  rare cases where users were relying on :tacn:`rapply` inserting
+  exactly 15 underscores and no more, due to the lemma having a
+  completely unspecified codomain (and thus allowing for any number of
+  underscores), the tactic will now instead loop. (`#10760
+  <https://github.com/coq/coq/pull/10760>`_, by Jason Gross)
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/07-commands-and-options/11258-coherence.rst b/doc/changelog/07-commands-and-options/11258-coherence.rst
new file mode 100644
index 0000000000..f04a120417
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11258-coherence.rst
@@ -0,0 +1,10 @@
+- **Changed:**
+  The :cmd:`Coercion` command has been improved to check the coherence of the
+  inheritance graph. It checks whether a circular inheritance path of `C >-> C`
+  is convertible with the identity function or not, then report it as an
+  ambiguous path if it is not.  The new mechanism does not report ambiguous
+  paths that are redundant with others. For example, checking the ambiguity of
+  `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will
+  not be reported
+  (`#11258 <https://github.com/coq/coq/pull/11258>`_,
+  by Kazuhiko Sakaguchi).
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c3b197288f..19b33f0d90 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -165,6 +165,12 @@ Declaring Coercions
      convertible with existing ones when they have coercions that don't satisfy
      the uniform inheritance condition.
 
+  .. warn:: ... is not definitionally an identity function.
+
+     If a coercion path has the same source and target class, that is said to be
+     circular. When a new circular coercion path is not convertible with the
+     identity function, it will be reported as ambiguous.
+
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
      Declares the construction denoted by :token:`qualid` as a coercion local to
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index bcdf3277ad..1424b4f3e1 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -60,7 +60,7 @@ Nonetheless, the manual has some structure that is explained below.
    of the formalism. Chapter :ref:`themodulesystem` describes the module
    system.
 
--  The second part describes the proof engine. It is divided in six
+-  The second part describes the proof engine. It is divided into several
    chapters. Chapter :ref:`vernacularcommands` presents all commands (we
    call them *vernacular commands*) that are not directly related to
    interactive proving: requests to the environment, complete or partial
@@ -68,8 +68,10 @@ Nonetheless, the manual has some structure that is explained below.
    proofs, do multiple proofs in parallel is explained in
    Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that
    realize one or more steps of the proof are presented: we call them
-   *tactics*. The language to combine these tactics into complex proof
-   strategies is given in Chapter :ref:`ltac`. Examples of tactics
+   *tactics*. The legacy language to combine these tactics into complex proof
+   strategies is given in Chapter :ref:`ltac`. The currently experimental
+   language that will eventually replace Ltac is presented in
+   Chapter :ref:`ltac2`. Examples of tactics
    are described in Chapter :ref:`detailedexamplesoftactics`.
    Finally, the |SSR| proof language is presented in
    Chapter :ref:`thessreflectprooflanguage`.
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index cfdc70d50e..dd80b29bda 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1,12 +1,12 @@
 .. _ltac2:
 
+Ltac2
+=====
+
 .. coqtop:: none
 
    From Ltac2 Require Import Ltac2.
 
-Ltac2
-=====
-
 The Ltac tactic language is probably one of the ingredients of the success of
 Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 81e50c0834..53cfb973d4 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
 
@@ -685,6 +688,28 @@ Applying theorems
       instantiate (see :ref:`Existential-Variables`). The instantiation is
       intended to be found later in the proof.
 
+   .. tacv:: rapply @term
+      :name: rapply
+
+      The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it
+      uses the proof engine of :tacn:`refine` for dealing with
+      existential variables, holes, and conversion problems.  This may
+      result in slightly different behavior regarding which conversion
+      problems are solvable.  However, like :tacn:`apply` but unlike
+      :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes
+      which remain in :n:`@term` itself after typechecking and
+      typeclass resolution but before unification with the goal.  More
+      technically, :n:`@term` is first parsed as a
+      :production:`constr` rather than as a :production:`uconstr` or
+      :production:`open_constr` before being applied to the goal. Note
+      that :tacn:`rapply` prefers to instantiate as many hypotheses of
+      :n:`@term` as possible.  As a result, if it is possible to apply
+      :n:`@term` to arbitrarily many arguments without getting a type
+      error, :tacn:`rapply` will loop.
+
+      Note that you need to :n:`Require Import Coq.Program.Tactics` to
+      make use of :tacn:`rapply`.
+
    .. tacv:: simple apply @term.
 
       This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms
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