Merge PR #10076: [Canonical structures] Annotation to field declarations to prevent them from being “canonical”

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: robbertkrebbers
Ack-by: vbgl

1 files changed, 19 insertions, 0 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 5308330820..ba766c8c3d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2048,6 +2048,21 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
 
+   .. note::
+      To prevent a field from being involved in the inference of canonical instances,
+      its declaration can be annotated with the :g:`#[canonical(false)]` attribute.
+
+      .. example::
+
+         For instance, when declaring the :g:`Setoid` structure above, the
+         :g:`Prf_equiv` field declaration could be written as follows.
+
+         .. coqdoc::
+
+            #[canonical(false)] Prf_equiv : equivalence Carrier Equal
+
+      See :ref:`canonicalstructures` for a more realistic example.
+
    .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term
 
       This is equivalent to a regular definition of :token:`ident` followed by the
@@ -2067,6 +2082,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          Print Canonical Projections.
 
+      .. note::
+
+         The last line would not show up if the corresponding projection (namely
+         :g:`Prf_equiv`) were annotated as not canonical, as described above.
 
 Implicit types of variables
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~