diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/07-commands-and-options/11164-let-cs.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 7 |
4 files changed, 22 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 diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 6884b6e998..0527e26353 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -490,6 +490,13 @@ The following example script illustrates all these features: You just finished a goal focused by ``{``, you must unfocus it with ``}``. +Mandatory Bullets +````````````````` + +Using :opt:`Default Goal Selector` with the ``!`` selector forces +tactic scripts to keep focus to exactly one goal (e.g. using bullets) +or use explicit goal selectors. + Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } |