diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 11 |
2 files changed, 14 insertions, 0 deletions
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 |