Merge PR #11164: [CS] allow Let variable to be canonical

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot

3 files changed, 15 insertions, 0 deletions

diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst
new file mode 100644
index 0000000000..b9ecd140e7
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst
@@ -0,0 +1 @@
+- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index e746096df2..bdfdffeaad 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1983,6 +1983,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
 ~~~~~~~~~~~~~~~~~~~~
 
@@ -1993,6 +1995,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 70dadedd35..d591718b17 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1620,6 +1620,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