Merge PR #10747: Extend `Print Canonical Projections` with a search functionality

Reviewed-by: CohenCyril
Ack-by: SkySkimmer
Reviewed-by: ejgallego

2 files changed, 16 insertions, 4 deletions

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/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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~