diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 61 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 63 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 |
3 files changed, 63 insertions, 65 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index e136252863..ac6a20198d 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -103,7 +103,7 @@ Special tokens ! % & && ( () ) * + ++ , - -> . .( .. / /\ : :: :< := :> ; < <- <-> <: <= <> = => =_D > >-> >= ? ?= @ [ \/ ] ^ { | |- - || } ~ + || } ~ #[ Lexical ambiguities are resolved according to the “longest match” rule: when a sequence of non alphanumerical characters can be @@ -495,6 +495,7 @@ The Vernacular ============== .. productionlist:: coq + decorated-sentence : [`decoration`] `sentence` sentence : `assumption` : | `definition` : | `inductive` @@ -523,6 +524,11 @@ The Vernacular proof : Proof . … Qed . : | Proof . … Defined . : | Proof . … Admitted . + decoration : #[ `attributes` ] + attributes : [`attribute`, … , `attribute`] + attribute : `ident` + :| `ident` = `string` + :| `ident` ( `attributes` ) .. todo:: This use of … in this grammar is inconsistent What about removing the proof part of this grammar from this chapter @@ -534,6 +540,9 @@ commands of Gallina. A sentence of the vernacular language, like in many natural languages, begins with a capital letter and ends with a dot. +Sentences may be *decorated* with so-called *attributes*, +which are described in the corresponding section (:ref:`gallina-attributes`). + The different kinds of command are described hereafter. They all suppose that the terms occurring in the sentences are well-typed. @@ -1388,3 +1397,53 @@ using the keyword :cmd:`Qed`. .. [2] Except if the inductive type is empty in which case there is no equation that can be used to infer the return type. + +.. _gallina-attributes: + +Attributes +----------- + +Any vernacular command can be decorated with a list of attributes, enclosed +between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket) +and separated by commas ``,``. + +Each attribute has a name (an identifier) and may have a value. +A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), +or a list of attributes, enclosed within brackets. + +Currently, +the following attributes names are recognized: + +``monomorphic``, ``polymorphic`` + Take no value, analogous to the ``Monomorphic`` and ``Polymorphic`` flags + (see :ref:`polymorphicuniverses`). + +``program`` + Takes no value, analogous to the ``Program`` flag + (see :ref:`programs`). + +``global``, ``local`` + Take no value, analogous to the ``Global`` and ``Local`` flags + (see :ref:`controlling-locality-of-commands`). + +``deprecated`` + Takes as value the optional attributes ``since`` and ``note``; + both have a string value. + +Here are a few examples: + +.. coqtop:: all reset + + From Coq Require Program. + #[program] Definition one : nat := S _. + Next Obligation. + exact O. + Defined. + + #[deprecated(since="8.9.0", note="use idtac instead")] + Ltac foo := idtac. + + Goal True. + Proof. + now foo. + Abort. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5dba92429e..bdaa2aa1a2 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -950,71 +950,10 @@ There are options to produce the |Coq| parts in smaller font, italic, between horizontal rules, etc. See the man page of ``coq-tex`` for more details. -|Coq| and GNU Emacs ------------------------ - - -The |Coq| Emacs mode -~~~~~~~~~~~~~~~~~~~~~~~~~ - -|Coq| comes with a Major mode for GNU Emacs, ``gallina.el``. This mode -provides syntax highlighting and also a rudimentary indentation -facility in the style of the ``Caml`` GNU Emacs mode. - -Add the following lines to your ``.emacs`` file: - -:: - - (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) - - -The |Coq| major mode is triggered by visiting a file with extension ``.v``, -or manually with the command ``M-x coq-mode``. It gives you the correct -syntax table for the |Coq| language, and also a rudimentary indentation -facility: - - -+ pressing ``Tab`` at the beginning of a line indents the line like the - line above; -+ extra tabulations increase the indentation level (by 2 spaces by default); -+ ``M-Tab`` decreases the indentation level. - - -An inferior mode to run |Coq| under Emacs, by Marco Maggesi, is also -included in the distribution, in file ``inferior-coq.el``. Instructions to -use it are contained in this file. - - -Proof-General -~~~~~~~~~~~~~ - -Proof-General is a generic interface for proof assistants based on -Emacs. The main idea is that the |Coq| commands you are editing are sent -to a |Coq| toplevel running behind Emacs and the answers of the system -automatically inserted into other Emacs buffers. Thus you don’t need -to copy-paste the |Coq| material from your files to the |Coq| toplevel or -conversely from the |Coq| toplevel to some files. - -Proof-General is developed and distributed independently of the system -|Coq|. It is freely available at `<https://proofgeneral.github.io/>`_. - - -Module specification --------------------- - -Given a |Coq| vernacular file, the gallina filter extracts its -specification (inductive types declarations, definitions, type of -lemmas and theorems), removing the proofs parts of the file. The |Coq| -file ``file.v`` gives birth to the specification file ``file.g`` (where -the suffix ``.g`` stands for |Gallina|). - -See the man page of ``gallina`` for more details and options. - Man pages --------- -There are man pages for the commands ``coqdep``, ``gallina`` and ``coq-tex``. Man +There are man pages for the commands ``coqdep`` and ``coq-tex``. Man pages are installed at installation time (see installation instructions in file ``INSTALL``, step 6). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 45667b0992..ec085a71e5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1418,7 +1418,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) dependent in the goal after application of :n:`destruct`, it is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). - + If term is a num, then destruct num behaves asintros until num + + If term is a num, then destruct num behaves as intros until num followed by destruct applied to the last introduced hypothesis. .. note:: @@ -4190,7 +4190,7 @@ datatype: see :ref:`quote` for the full details. Happens when quote is not able to perform inversion properly. -.. tacv:: quote ident {* @ident} +.. tacv:: quote @ident {* @ident} All terms that are built only with :n:`{* @ident}` will be considered by quote as constants rather than variables. |