[Attributes] accept #[canonical] (Let|Definition)

2 files changed, 14 insertions, 0 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8caa289a47..05e4cf1346 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1994,6 +1994,8 @@ Deactivation of implicit arguments for parsing
    to be given as if no arguments were implicit. By symmetry, this also
    affects printing.
 
+.. _canonical-structure-declaration:
+
 Canonical structures
 ~~~~~~~~~~~~~~~~~~~~
 
@@ -2004,6 +2006,7 @@ value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
 .. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid
+  :name: Canonical Structure
 
    This command declares :token:`qualid` as a canonical instance of a
    structure (a record). When the :g:`#[local]` attribute is given the effect
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 3cc101d06b..ac34fc707a 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1691,6 +1691,17 @@ variety of commands:
        :n:`@string__1` is the actual notation, :n:`@string__2` is the version number,
        :n:`@string__3` is the note.
 
+``canonical``
+    This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command.
+    It is equivalent to having a :cmd:`Canonical Structure` declaration just
+    after the command.
+
+    This attirbute can take the value ``false`` when decorating a record field
+    declaration with the effect of preventing the field from being involved in
+    the inference of canonical instances.
+
+    See also :ref:`canonical-structure-declaration`.
+
 .. example::
 
    .. coqtop:: all reset warn