8 files changed, 65 insertions, 10 deletions
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/11288-omega+depr.rst b/doc/changelog/04-tactics/11288-omega+depr.rst
new file mode 100644
index 0000000000..2832e6db61
--- /dev/null
+++ b/doc/changelog/04-tactics/11288-omega+depr.rst
@@ -0,0 +1,6 @@
+- **Removed:**
+  The undocumented ``omega with`` tactic variant has been removed,
+  using ``lia`` is the recommended replacement, tho the old semantics
+  of ``omega with *`` can be recovered with ``zify; omega``
+  (`#11288 <https://github.com/coq/coq/pull/11288>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/04-tactics/11337-omega-with-depr.rst b/doc/changelog/04-tactics/11337-omega-with-depr.rst
new file mode 100644
index 0000000000..25e929e030
--- /dev/null
+++ b/doc/changelog/04-tactics/11337-omega-with-depr.rst
@@ -0,0 +1,6 @@
+- **Deprecated:**
+  The undocumented ``omega with`` tactic variant has been deprecated,
+  using ``lia`` is the recommended replacement, tho the old semantics
+  of ``omega with *`` can be recovered with ``zify; omega``
+  (`#11337 <https://github.com/coq/coq/pull/11337>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
new file mode 100644
index 0000000000..e73be9c642
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  The :cmd:`Print Canonical Projections` command now can take constants and
+  prints only the unification rules that involve or are synthesized from given
+  constants (`#10747 <https://github.com/coq/coq/pull/10747>`_,
+  by Kazuhiko Sakaguchi).
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/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8caa289a47..a8d6d2632b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2075,11 +2075,13 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       This is equivalent to a regular definition of :token:`ident` followed by the
       declaration :n:`Canonical @ident`.
 
-.. cmd:: Print Canonical Projections
+.. cmd:: Print Canonical Projections {* @ident}
 
    This displays the list of global names that are components of some
    canonical structure. For each of them, the canonical structure of
-   which it is a projection is indicated.
+   which it is a projection is indicated. If constants are given as
+   its arguments, only the unification rules that involve or are
+   synthesized from simultaneously all given constants will be shown.
 
    .. example::
 
@@ -2089,10 +2091,15 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          Print Canonical Projections.
 
+      .. coqtop:: all
+
+         Print Canonical Projections nat.
+
       .. note::
 
-         The last line would not show up if the corresponding projection (namely
-         :g:`Prf_equiv`) were annotated as not canonical, as described above.
+         The last line in the first example would not show up if the
+         corresponding projection (namely :g:`Prf_equiv`) were annotated as not
+         canonical, as described above.
 
 Implicit types of variables
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 878118c48a..53cfb973d4 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -688,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