[sphinx] Finish clean-up of the Canonical Structure subsection.

1 files changed, 32 insertions, 40 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 1a57e5419..c21d8d4ec 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1925,69 +1925,61 @@ applied to an unknown structure instance (an implicit argument) and a
 value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
-Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in the
-structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that
-`qualid` is declared as a canonical structure using the command
-
 .. cmd:: Canonical Structure @qualid
 
-Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
-solved during the type-checking process, `qualid` is used as a solution.
-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.
-
-.. example::
-
-   Here is an example.
+   This command declares :token:`qualid` as a canonical structure.
 
-   .. coqtop:: all
+   Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
+   structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
+   Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
+   solved during the type-checking process, :token:`qualid` is used as a solution.
+   Otherwise said, :token:`qualid` is canonically used to extend the field |c_i|
+   into a complete structure built on |c_i|.
 
-      Require Import Relations.
+   Canonical structures are particularly useful when mixed with coercions
+   and strict implicit arguments.
 
-      Require Import EqNat.
+   .. example::
 
-      Set Implicit Arguments.
+      Here is an example.
 
-      Unset Strict Implicit.
+      .. coqtop:: all
 
-      Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
-                                  Prf_equiv : equivalence Carrier Equal}.
+         Require Import Relations.
 
-      Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
+         Require Import EqNat.
 
-      Axiom eq_nat_equiv : equivalence nat eq_nat.
+         Set Implicit Arguments.
 
-      Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
+         Unset Strict Implicit.
 
-      Canonical Structure nat_setoid.
+         Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
+                                     Prf_equiv : equivalence Carrier Equal}.
 
-Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A``
-and ``B`` can be synthesized in the next statement.
+         Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
 
-.. coqtop:: all
+         Axiom eq_nat_equiv : equivalence nat eq_nat.
 
-   Lemma is_law_S : is_law S.
+         Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
 
-Remark: If a same field occurs in several canonical structure, then
-only the structure declared first as canonical is considered.
+         Canonical Structure nat_setoid.
 
-.. cmdv:: Canonical Structure @ident := @term : @type
+      Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A`
+      and :g:`B` can be synthesized in the next statement.
 
-.. cmdv:: Canonical Structure @ident := @term
+      .. coqtop:: all
 
-.. cmdv:: Canonical Structure @ident : @type := @term
+         Lemma is_law_S : is_law S.
 
-These are equivalent to a regular definition of `ident` followed by the declaration
-``Canonical Structure`` `ident`.
+   .. note::
+      If a same field occurs in several canonical structures, then
+      only the structure declared first as canonical is considered.
 
-See also: more examples in user contribution category (Rocq/ALGEBRA).
+   .. cmdv:: Canonical Structure @ident {? : @type } := @term
 
+      This is equivalent to a regular definition of :token:`ident` followed by the
+      declaration :n:`Canonical Structure @ident`.
 
-Printing Canonical Projections
-++++++++++++++++++++++++++++++
 
 .. cmd:: Print Canonical Projections