From ad314b4291d85697831161a7abef6f00a4d37c1f Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Thu, 14 Jun 2018 18:43:00 +0200
Subject: doc: Add "Print Canonical Projections" command to Command index

---
 doc/sphinx/language/gallina-extensions.rst | 49 ++++++++++++++++++------------
 1 file changed, 29 insertions(+), 20 deletions(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ff5d352c99..1a57e54196 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
-- 
cgit v1.2.3


From 8c64c9e2479fe12634a22b4c90da12a24833e9bc Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 16 Jun 2018 14:56:22 +0200
Subject: [sphinx] Finish clean-up of the Canonical Structure subsection.

---
 doc/sphinx/language/gallina-extensions.rst | 72 +++++++++++++-----------------
 1 file changed, 32 insertions(+), 40 deletions(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 1a57e54196..c21d8d4ec8 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
 
-- 
cgit v1.2.3