doc: Add "Print Canonical Projections" command to Command index

1 files changed, 29 insertions, 20 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ff5d352c9..1a57e5419 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1937,28 +1937,32 @@ Otherwise said, `qualid` is canonically used to extend the field |c_i|
 into a complete structure built on |c_i|.
 
 Canonical structures are particularly useful when mixed with coercions
-and strict implicit arguments. Here is an example.
+and strict implicit arguments.
 
-.. coqtop:: all
+.. example::
+
+   Here is an example.
 
-   Require Import Relations.
+   .. coqtop:: all
 
-   Require Import EqNat.
+      Require Import Relations.
 
-   Set Implicit Arguments.
+      Require Import EqNat.
 
-   Unset Strict Implicit.
+      Set Implicit Arguments.
 
-   Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
-                               Prf_equiv : equivalence Carrier Equal}.
+      Unset Strict Implicit.
 
-   Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
+      Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
+                                  Prf_equiv : equivalence Carrier Equal}.
 
-   Axiom eq_nat_equiv : equivalence nat eq_nat.
+      Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
 
-   Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
+      Axiom eq_nat_equiv : equivalence nat eq_nat.
 
-   Canonical Structure nat_setoid.
+      Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
+
+      Canonical Structure nat_setoid.
 
 Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A``
 and ``B`` can be synthesized in the next statement.
@@ -1982,17 +1986,22 @@ These are equivalent to a regular definition of `ident` followed by the declarat
 See also: more examples in user contribution category (Rocq/ALGEBRA).
 
 
-Print Canonical Projections.
-++++++++++++++++++++++++++++
+Printing Canonical Projections
+++++++++++++++++++++++++++++++
 
-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. For instance, the above example
-gives the following output:
+.. cmd:: Print Canonical Projections
 
-.. coqtop:: all
+   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.
+
+   .. example::
+
+      For instance, the above example gives the following output:
+
+      .. coqtop:: all
 
-   Print Canonical Projections.
+         Print Canonical Projections.
 
 
 Implicit types of variables