diff options
Diffstat (limited to 'doc')
38 files changed, 807 insertions, 620 deletions
diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst index 638222fbe1..b89e047153 100644 --- a/doc/changelog/07-commands-and-options/11162-local-cs.rst +++ b/doc/changelog/07-commands-and-options/11162-local-cs.rst @@ -1,3 +1,3 @@ -- **Added:** Handle the ``#[local]`` attribute in :g:`Canonical +- **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical Structure` declarations (`#11162 <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst b/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst new file mode 100644 index 0000000000..d134aeae8b --- /dev/null +++ b/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst @@ -0,0 +1,5 @@ +- **Removed:** Deprecated unsound compatibility ``Template Check`` + flag that was introduced in 8.10 to help users gradually move their + template polymorphic inductive type definitions outside sections + (`#11546 <https://github.com/coq/coq/pull/11546>`_, by Pierre-Marie + Pédrot). diff --git a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst index 1f8dcd3992..419d683037 100644 --- a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst +++ b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst @@ -1,5 +1,6 @@ - **Removed:** Unqualified ``polymorphic``, ``monomorphic``, ``template``, ``notemplate`` attributes (they were deprecated since Coq 8.10). - Use them as sub-attributes of the ``universes`` attribute (`#11663 - <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). + Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, + :attr:`universes(template)` and :attr:`universes(notemplate)` instead + (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). diff --git a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst new file mode 100644 index 0000000000..b6a034941d --- /dev/null +++ b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst @@ -0,0 +1,12 @@ +- **Added:** + New attributes supported when defining an inductive type + :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`private(matching)`, which correspond to legacy attributes + ``Cumulative``, ``NonCumulative``, and the so far undocumented + ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by + Théo Zimmermann). + +- **Changed:** + Legacy attributes can now be passed in any order. See + :ref:`gallina-attributes` (`#11665 + <https://github.com/coq/coq/pull/11665>`_, by Théo Zimmermann). diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst new file mode 100644 index 0000000000..a07e48d2d8 --- /dev/null +++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst @@ -0,0 +1,6 @@ +- **Changed:** + The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc. + and the option set flags `-set`, `-unset` are processed have been reversed. + In the new behavior, require/load flags are processed before option flags. + (`#11851 <https://github.com/coq/coq/pull/11851>`_, + by Lasse Blaauwbroek). @@ -1,5 +1,10 @@ (rule - (targets sphinx_build) + (targets unreleased.rst) + (deps (source_tree changelog)) + (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) + +(alias + (name refman-deps) (deps ; We could use finer dependencies here so the build is faster: ; @@ -10,23 +15,34 @@ ; + tools/coqdoc/coqdoc.css (package coq) (source_tree sphinx) - (source_tree tools) + (source_tree tools/coqrst) unreleased.rst - (env_var SPHINXWARNOPT)) - (action - (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (env_var SPHINXWARNOPT))) -(alias - (name refman-html) - (deps sphinx_build)) +(rule + (targets refman-html) + (alias refman-html) + (package coq-doc) + (deps (alias refman-deps)) + (action + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets}))) (rule - (targets unreleased.rst) - (deps (source_tree changelog)) - (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) + (targets refman-pdf) + (alias refman-pdf) + (package coq-doc) + (deps (alias refman-deps)) + (action + (progn + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets}) + (chdir %{targets} (run make))))) + +; Installable directories are not yet fully supported by Dune. See +; ocaml/dune#1868. Yet, this makes coq-doc.install a valid target to +; generate the whole Coq documentation. And the result under +; _build/install/default/doc/coq-doc looks just right! -; The install target still needs more work. -; (install -; (section doc) -; (package coq-refman) -; (files sphinx_build)) +(install + (files (refman-html as html/refman) (refman-pdf as pdf/refman)) + (section doc) + (package coq-doc)) diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index d909f98956..41b726b069 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,7 +1,7 @@ .. _extraction: -Extraction of programs in |OCaml| and Haskell -============================================= +Program extraction +================== :Authors: Jean-Christophe Filliâtre and Pierre Letouzey diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index db8c09d88f..0e8660cb0e 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,10 +1,5 @@ -.. _miscellaneousextensions: - -Miscellaneous extensions -======================== - Program derivation ------------------- +================== |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 549249d25c..cbb5c0db8a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -98,10 +98,17 @@ coercions. .. flag:: Program Mode Enables the program mode, in which 1) typechecking allows subset coercions and - 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and - :cmd:`Program Definition` act - like Program Fixpoint/Definition, generating obligations if there are - unresolved holes after typechecking. + 2) the elaboration of pattern matching of :cmd:`Fixpoint` and + :cmd:`Definition` act as if the :attr:`program` attribute had been + used, generating obligations if there are unresolved holes after + typechecking. + +.. attr:: program + + This attribute allows to use the Program mode on a specific + definition. An alternative syntax is to use the legacy ``Program`` + prefix (cf. :n:`@legacy_attr`) as documented in the rest of this + chapter. .. _syntactic_control: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 7abeca7815..bd4c276571 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -47,7 +47,7 @@ Leibniz equality on some type. An example implementation is: | tt, tt => eq_refl tt end }. -Using the attribute ``refine``, if the term is not sufficient to +Using the :attr:`refine` attribute, if the term is not sufficient to finish the definition (e.g. due to a missing field or non-inferable hole) it must be finished in proof mode. If it is sufficient a trivial proof mode with no open goals is started. @@ -77,9 +77,9 @@ remaining fields, e.g.: Defined. One has to take care that the transparency of every field is -determined by the transparency of the :cmd:`Instance` proof. One can use -alternatively the :cmd:`Program Instance` variant which has richer facilities -for dealing with obligations. +determined by the transparency of the :cmd:`Instance` proof. One can +use alternatively the :attr:`program` attribute to get richer +facilities for dealing with obligations. Binding classes @@ -174,7 +174,7 @@ For example: .. coqtop:: in - Global Program Instance option_eqb : EqDec (option A) := + #[ global, program ] Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true @@ -188,7 +188,7 @@ For example: About option_eqb. -Here the :cmd:`Global` modifier redeclares the instance at the end of the +Here the :attr:`global` attribute redeclares the instance at the end of the section, once it has been generalized by the context variables it uses. @@ -300,9 +300,11 @@ Summary of the commands The :cmd:`Class` command is used to declare a typeclass with parameters :token:`binders` and fields the declared record fields. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, + Like any command declaring a record, this command supports the + :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`private(matching)` attributes. .. _singleton-class: @@ -341,6 +343,25 @@ Summary of the commands :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number of non-dependent binders of the instance. + This command supports the :attr:`global` attribute that can be + used on instances declared in a section so that their + generalization is automatically redeclared after the section is + closed. + + Like :cmd:`Definition`, it also supports the :attr:`program` + attribute to switch the type checking to `Program` (chapter + :ref:`programs`) and use the obligation mechanism to manage missing + fields. + + Finally, it supports the lighter :attr:`refine` attribute: + + .. attr:: refine + + This attribute can be used to leave holes or not provide all + fields in the definition of an instance and open the tactic mode + to fill them. It works exactly as if no body had been given and + the :tacn:`refine` tactic has been used first. + .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term This syntax is used for declaration of singleton class instances or @@ -348,19 +369,6 @@ Summary of the commands {+ @term}`. One need not even mention the unique field name for singleton classes. - .. cmdv:: Global Instance - :name: Global Instance - - One can use the :cmd:`Global` modifier on instances declared in a - section so that their generalization is automatically redeclared - after the section is closed. - - .. cmdv:: Program Instance - :name: Program Instance - - Switches the type checking to `Program` (chapter :ref:`programs`) and - uses the obligation mechanism to manage missing fields. - .. cmdv:: Declare Instance :name: Declare Instance diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 0e326f45d2..a08495badd 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,62 +122,92 @@ in a universe strictly higher than :g:`Set`. Polymorphic, Monomorphic ------------------------- -.. cmd:: Polymorphic @definition +.. attr:: universes(polymorphic) - As shown in the examples, polymorphic definitions and inductives can be - declared using the ``Polymorphic`` prefix. + This attribute can be used to declare universe polymorphic + definitions and inductive types. There is also a legacy syntax + using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as + shown in the examples, is more commonly used. .. flag:: Universe Polymorphism - Once enabled, this flag will implicitly prepend ``Polymorphic`` to any - definition of the user. + This flag is off by default. When it is on, new declarations are + polymorphic unless the :attr:`universes(monomorphic)` attribute is + used. -.. cmd:: Monomorphic @definition +.. attr:: universes(monomorphic) - When the :flag:`Universe Polymorphism` flag is set, to make a definition - producing global universe constraints, one can use the ``Monomorphic`` prefix. + This attribute can be used to declare universe monomorphic + definitions and inductive types (i.e. global universe constraints + are produced), even when the :flag:`Universe Polymorphism` flag is + on. There is also a legacy syntax using the ``Monomorphic`` prefix + (see :n:`@legacy_attr`). -Many other commands support the ``Polymorphic`` flag, including: +Many other commands can be used to declare universe polymorphic or +monomorphic constants depending on whether the :flag:`Universe +Polymorphism` flag is on or the :attr:`universes(polymorphic)` or +:attr:`universes(monomorphic)` attributes are used: -.. TODO add links on each of these? +- :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe + polymorphic constants. -- ``Lemma``, ``Axiom``, and all the other “definition” keywords support - polymorphism. +- Using the :attr:`universes(polymorphic)` attribute with the + :cmd:`Section` command will locally set the polymorphism flag inside + the section. -- :cmd:`Section` will locally set the polymorphism flag inside the section. +- :cmd:`Variable`, :cmd:`Context`, :cmd:`Universe` and + :cmd:`Constraint` in a section support polymorphism. See + :ref:`universe-polymorphism-in-sections` for more details. -- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support - polymorphism. See :ref:`universe-polymorphism-in-sections` for more details. - -- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint - polymorphically, not at a single instance. +- Using the :attr:`universes(polymorphic)` attribute with the + :cmd:`Hint Resolve` or :cmd:`Hint Rewrite` commands will make + :tacn:`auto` / :tacn:`rewrite` use the hint polymorphically, not at + a single instance. .. _cumulative: Cumulative, NonCumulative ------------------------- -Polymorphic inductive types, coinductive types, variants and records can be -declared cumulative using the :g:`Cumulative` prefix. +.. attr:: universes(cumulative) + + Polymorphic inductive types, coinductive types, variants and + records can be declared cumulative using this attribute or the + legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as + shown in the examples, is more commonly used. -.. cmd:: Cumulative @inductive + This means that two instances of the same inductive type (family) + are convertible based on the universe variances; they do not need + to be equal. - Declares the inductive as cumulative + .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. -Alternatively, there is a :flag:`Polymorphic Inductive -Cumulativity` flag which when set, makes all subsequent *polymorphic* -inductive definitions cumulative. When set, inductive types and the -like can be enforced to be non-cumulative using the :g:`NonCumulative` -prefix. + Using this attribute requires being in a polymorphic context, + i.e. either having the :flag:`Universe Polymorphism` flag on, or + having used the :attr:`universes(polymorphic)` attribute as + well. -.. cmd:: NonCumulative @inductive + .. note:: - Declares the inductive as non-cumulative + ``#[ universes(polymorphic), universes(cumulative) ]`` can be + abbreviated into ``#[ universes(polymorphic, cumulative) ]``. .. flag:: Polymorphic Inductive Cumulativity - When this flag is on, it sets all following polymorphic inductive - types as cumulative (it is off by default). + When this flag is on (it is off by default), it makes all + subsequent *polymorphic* inductive definitions cumulative, unless + the :attr:`universes(noncumulative)` attribute is used. It has no + effect on *monomorphic* inductive definitions. + +.. attr:: universes(noncumulative) + + Declares the inductive type as non-cumulative even if the + :flag:`Polymorphic Inductive Cumulativity` flag is on. There is + also a legacy syntax using the ``NonCumulative`` prefix (see + :n:`@legacy_attr`). + + This means that two instances of the same inductive type (family) + are convertible only if all the universes are equal. Consider the examples below. @@ -220,34 +250,10 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j -Cumulative inductive types, coinductive types, variants and records -only make sense when they are universe polymorphic. Therefore, an -error is issued whenever the user uses the :g:`Cumulative` or -:g:`NonCumulative` prefix in a monomorphic context. -Notice that this is not the case for the :flag:`Polymorphic Inductive Cumulativity` flag. -That is, this flag, when set, makes all subsequent *polymorphic* -inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) -but has no effect on *monomorphic* inductive declarations. - -Consider the following examples. - -.. coqtop:: all reset - - Fail Monomorphic Cumulative Inductive Unit := unit. - -.. coqtop:: all reset - - Fail Monomorphic NonCumulative Inductive Unit := unit. - -.. coqtop:: all reset - - Set Polymorphic Inductive Cumulativity. - Inductive Unit := unit. - An example of a proof using cumulativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. coqtop:: in +.. coqtop:: in reset Set Universe Polymorphism. Set Polymorphic Inductive Cumulativity. @@ -368,10 +374,14 @@ to universes and explicitly instantiate polymorphic definitions. In the monorphic case, this command declares a new global universe named :g:`ident`, which can be referred to using its qualified name as well. Global universe names live in a separate namespace. The - command supports the ``Polymorphic`` flag only in sections, meaning the - universe quantification will be discharged on each section definition + command supports the :attr:`universes(polymorphic)` attribute (or + the ``Polymorphic`` prefix) only in sections, meaning the universe + quantification will be discharged on each section definition independently. + .. exn:: Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead. + :undocumented: + .. cmd:: Constraint @univ_constraint Polymorphic Constraint @univ_constraint @@ -379,9 +389,10 @@ to universes and explicitly instantiate polymorphic definitions. If consistent, the constraint is then enforced in the global environment. Like :cmd:`Universe`, it can be used with the - ``Polymorphic`` prefix in sections only to declare constraints - discharged at section closing time. One cannot declare a global - constraint on polymorphic universes. + :attr:`universes(polymorphic)` attribute (or the ``Polymorphic`` + prefix) in sections only to declare constraints discharged at + section closing time. One cannot declare a global constraint on + polymorphic universes. .. exn:: Undeclared universe @ident. :undocumented: @@ -389,6 +400,9 @@ to universes and explicitly instantiate polymorphic definitions. .. exn:: Universe inconsistency. :undocumented: + .. exn:: Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead + :undocumented: + Polymorphic definitions ~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/appendix/history-and-changes/index.rst b/doc/sphinx/appendix/history-and-changes/index.rst new file mode 100644 index 0000000000..50ffec8e3f --- /dev/null +++ b/doc/sphinx/appendix/history-and-changes/index.rst @@ -0,0 +1,21 @@ +.. _history-and-changes: + +========================== +History and recent changes +========================== + +This chapter is divided in two parts. The first one is about the +:ref:`early history of Coq <history>` and is presented in +chronological order. The second one provides :ref:`release notes +about recent versions of Coq <changes>` and is presented in reverse +chronological order. When updating your copy of Coq to a new version +(especially a new major version), it is strongly recommended that you +read the corresponding release notes. They may contain advice that +will help you understand the differences with the previous version and +upgrade your projects. + +.. toctree:: + :maxdepth: 1 + + ../../history + ../../changes diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst new file mode 100644 index 0000000000..a5032ff822 --- /dev/null +++ b/doc/sphinx/appendix/indexes/index.rst @@ -0,0 +1,24 @@ +:orphan: + +.. _indexes: + +======== +Indexes +======== + +We provide various specialized indexes that are helpful to quickly +find what you are looking for. + +.. toctree:: + + ../../genindex + ../../coq-cmdindex + ../../coq-tacindex + ../../coq-optindex + ../../coq-exnindex + +For reference, here are direct links to the documentation of: + +- :ref:`flags, options and tables <flags-options-tables>`; +- controlling the display of warning messages with the :opt:`Warnings` + option. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6d9979a704..a0cf9730a9 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -1,3 +1,5 @@ +.. _changes: + -------------- Recent changes -------------- @@ -220,7 +222,7 @@ Changes in 8.11+beta1 .. _811RefineInstance: -- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more +- **Added:** :attr:`refine` attribute for :cmd:`Instance`, a more predictable version of the old ``Refine Instance Mode`` which unconditionally opens a proof (`#10996 <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). @@ -1314,7 +1316,7 @@ Changes in 8.10+beta3 rules governing template-polymorphic types. To help users incrementally fix this issue, a command line option - `-no-template-check` and a global flag :flag:`Template Check` are + `-no-template-check` and a global flag ``Template Check`` are available to selectively disable the new check. Use at your own risk. (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 3d77d07061..c2c1c68f5c 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -186,9 +186,7 @@ nitpick_ignore = [ ('token', token) for token in [ 'assums', 'binders', 'collection', - 'definition', 'dirpath', - 'inductive', 'ind_body', 'modpath', 'module', diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst index 29f792b3aa..e3a27fd7c4 100644 --- a/doc/sphinx/genindex.rst +++ b/doc/sphinx/genindex.rst @@ -2,6 +2,6 @@ .. hack to get index in TOC ------ -Index ------ +------------- +General index +------------- diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst index c4a48d6985..153dc1f368 100644 --- a/doc/sphinx/history.rst +++ b/doc/sphinx/history.rst @@ -1,3 +1,5 @@ +.. _history: + -------------------- Early history of Coq -------------------- diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index 0a20d1c47b..6069ed42fe 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -8,84 +8,37 @@ Contents -------- .. toctree:: - :caption: Indexes - - genindex - coq-cmdindex - coq-tacindex - coq-optindex - coq-exnindex - -.. No entries yet - * :index:`thmindex` - -.. toctree:: - :caption: Preamble self - history - changes .. toctree:: - :caption: The language + :caption: Specification language - language/gallina-specification-language - language/gallina-extensions - language/coq-library - language/cic - language/module-system + language/core/index + language/extensions/index .. toctree:: - :caption: The proof engine + :caption: Proofs - proof-engine/vernacular-commands - proof-engine/proof-handling - proof-engine/tactics - proof-engine/ltac - proof-engine/ltac2 - proof-engine/detailed-tactic-examples - proof-engine/ssreflect-proof-language + proofs/writing-proofs/index + proofs/automatic-tactics/index + proofs/creating-tactics/index .. toctree:: - :caption: User extensions + :caption: Using Coq - user-extensions/syntax-extensions - user-extensions/proof-schemes + using/libraries/index + using/tools/index .. toctree:: - :caption: Practical tools + :caption: Appendix - practical-tools/coq-commands - practical-tools/utilities - practical-tools/coqide - -.. toctree:: - :caption: Addendum - - addendum/extended-pattern-matching - addendum/implicit-coercions - addendum/canonical-structures - addendum/type-classes - addendum/omega - addendum/micromega - addendum/extraction - addendum/program - addendum/ring - addendum/nsatz - addendum/generalized-rewriting - addendum/parallel-proof-processing - addendum/miscellaneous-extensions - addendum/universe-polymorphism - addendum/sprop + appendix/history-and-changes/index + appendix/indexes/index + zebibliography -.. toctree:: - :caption: Reference +.. No entries yet + * :index:`thmindex` - zebibliography .. include:: license.rst - -.. [#PG] Proof-General is available at https://proofgeneral.github.io/. - Optionally, you can enhance it with the minor mode - Company-Coq :cite:`Pit16` - (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 5562736997..62d9525194 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -10,81 +10,39 @@ Introduction .. include:: license.rst -.. [#PG] Proof-General is available at https://proofgeneral.github.io/. - Optionally, you can enhance it with the minor mode - Company-Coq :cite:`Pit16` - (see https://github.com/cpitclaudel/company-coq). - -.. include:: history.rst - -.. include:: changes.rst - ------------- -The language ------------- +---------------------- +Specification language +---------------------- .. toctree:: - language/gallina-specification-language - language/gallina-extensions - language/coq-library - language/cic - language/module-system + language/core/index + language/extensions/index ----------------- -The proof engine ----------------- +------ +Proofs +------ .. toctree:: - proof-engine/vernacular-commands - proof-engine/proof-handling - proof-engine/tactics - proof-engine/ltac - proof-engine/ltac2 - proof-engine/detailed-tactic-examples - proof-engine/ssreflect-proof-language + proofs/writing-proofs/index + proofs/automatic-tactics/index + proofs/creating-tactics/index ---------------- -User extensions ---------------- +--------- +Using Coq +--------- .. toctree:: - user-extensions/syntax-extensions - user-extensions/proof-schemes - ---------------- -Practical tools ---------------- - -.. toctree:: - - practical-tools/coq-commands - practical-tools/utilities - practical-tools/coqide + using/libraries/index + using/tools/index -------- -Addendum +Appendix -------- .. toctree:: - addendum/extended-pattern-matching - addendum/implicit-coercions - addendum/canonical-structures - addendum/type-classes - addendum/omega - addendum/micromega - addendum/extraction - addendum/program - addendum/ring - addendum/nsatz - addendum/generalized-rewriting - addendum/parallel-proof-processing - addendum/miscellaneous-extensions - addendum/universe-polymorphism - addendum/sprop - -.. toctree:: + appendix/history-and-changes/index zebibliography diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 1424b4f3e1..b059fb4069 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,107 +1,68 @@ -This document is the Reference Manual of the |Coq| proof assistant. -To start using Coq, it is advised to first read a tutorial. -Links to several tutorials can be found at -https://coq.inria.fr/documentation and -https://github.com/coq/coq/wiki#coq-tutorials - -The |Coq| system is designed to develop mathematical proofs, and -especially to write formal specifications, programs and to verify that -programs are correct with respect to their specifications. It provides a -specification language named |Gallina|. Terms of |Gallina| can represent -programs as well as properties of these programs and proofs of these -properties. Using the so-called *Curry-Howard isomorphism*, programs, -properties and proofs are formalized in the same language called -*Calculus of Inductive Constructions*, that is a -:math:`\lambda`-calculus with a rich type system. All logical judgments -in |Coq| are typing judgments. The very heart of the |Coq| system is the -type checking algorithm that checks the correctness of proofs, in other -words that checks that a program complies to its specification. |Coq| also -provides an interactive proof assistant to build proofs using specific -programs called *tactics*. - -All services of the |Coq| proof assistant are accessible by interpretation -of a command language called *the vernacular*. - -Coq has an interactive mode in which commands are interpreted as the -user types them in from the keyboard and a compiled mode where commands -are processed from a file. - -- In interactive mode, users can develop their theories and proofs step by - step, and query the system for available theorems and definitions. The - interactive mode is generally run with the help of an IDE, such - as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, - Emacs with Proof-General :cite:`Asp00` [#PG]_, - or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). - The `coqtop` read-eval-print-loop can also be used directly, for debugging - purposes. - -- The compiled mode acts as a proof checker taking a file containing a - whole development in order to ensure its correctness. Moreover, - |Coq|’s compiler provides an output file containing a compact - representation of its input. The compiled mode is run with the `coqc` - command. - -.. seealso:: :ref:`thecoqcommands`. - -How to read this book ---------------------- - -This is a Reference Manual, so it is not intended for continuous reading. -We recommend using the various indexes to quickly locate the documentation -you are looking for. There is a global index, and a number of specific indexes -for tactics, vernacular commands, and error messages and warnings. -Nonetheless, the manual has some structure that is explained below. - -- The first part describes the specification language, |Gallina|. - Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete - syntax as well as the meaning of programs, theorems and proofs in the - Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the - standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description - of the formalism. Chapter :ref:`themodulesystem` describes the module - system. - -- The second part describes the proof engine. It is divided into several - chapters. Chapter :ref:`vernacularcommands` presents all commands (we - call them *vernacular commands*) that are not directly related to - interactive proving: requests to the environment, complete or partial - evaluation, loading and compiling files. How to start and stop - proofs, do multiple proofs in parallel is explained in - Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that - realize one or more steps of the proof are presented: we call them - *tactics*. The legacy language to combine these tactics into complex proof - strategies is given in Chapter :ref:`ltac`. The currently experimental - language that will eventually replace Ltac is presented in - Chapter :ref:`ltac2`. Examples of tactics - are described in Chapter :ref:`detailedexamplesoftactics`. - Finally, the |SSR| proof language is presented in - Chapter :ref:`thessreflectprooflanguage`. - -- The third part describes how to extend the syntax of |Coq| in - Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define - new induction principles in Chapter :ref:`proofschemes`. - -- In the fourth part more practical tools are documented. First in - Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and - `coqtop` (interactive mode) with their options is described. Then, - in Chapter :ref:`utilities`, various utilities that come with the - |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` - describes CoqIDE. - -- The fifth part documents a number of advanced features, including coercions, - canonical structures, typeclasses, program extraction, and specialized - solvers and tactics. See the table of contents for a complete list. - -List of additional documentation --------------------------------- - -This manual does not contain all the documentation the user may need -about |Coq|. Various informations can be found in the following documents: - -Installation - A text file `INSTALL` that comes with the sources explains how to - install |Coq|. - -The |Coq| standard library - A commented version of sources of the |Coq| standard library - (including only the specifications, the proofs are removed) is - available at https://coq.inria.fr/stdlib/. +This is the reference manual of |Coq|. Coq is an interactive theorem +prover. It lets you formalize mathematical concepts and then helps +you interactively generate machine-checked proofs of theorems. +Machine checking gives users much more confidence that the proofs are +correct compared to human-generated and -checked proofs. Coq has been +used in a number of flagship verification projects, including the +`CompCert verified C compiler <http://compcert.inria.fr/>`_, and has +served to verify the proof of the `four color theorem +<https://github.com/math-comp/fourcolor>`_ (among many other +mathematical formalizations). + +Users generate proofs by entering a series of tactics that constitute +steps in the proof. There are many built-in tactics, some of which +are elementary, while others implement complex decision procedures +(such as :tacn:`lia`, a decision procedure for linear integer +arithmetic). :ref:`Ltac <ltac>` and its planned replacement, +:ref:`Ltac2 <ltac2>`, provide languages to define new tactics by +combining existing tactics with looping and conditional constructs. +These permit automation of large parts of proofs and sometimes entire +proofs. Furthermore, users can add novel tactics or functionality by +creating Coq plugins using OCaml. + +The Coq kernel, a small part of Coq, does the final verification that +the tactic-generated proof is valid. Usually the tactic-generated +proof is indeed correct, but delegating proof verification to the +kernel means that even if a tactic is buggy, it won't be able to +introduce an incorrect proof into the system. + +Finally, Coq also supports extraction of verified programs to +programming languages such as OCaml and Haskell. This provides a way +of executing Coq code efficiently and can be used to create verified +software libraries. + +To learn Coq, beginners are advised to first start with a tutorial / +book. Several such tutorials / books are listed at +https://coq.inria.fr/documentation. + +This manual is organized in three main parts, plus an appendix: + +- **The first part presents the specification language of Coq**, that + allows to define programs and state mathematical theorems. + :ref:`core-language` presents the language that the kernel of Coq + understands. :ref:`extensions` presents the richer language, with + notations, implicits, etc. that a user can use and which is + translated down to the language of the kernel by means of an + "elaboration process". + +- **The second part presents the interactive proof mode**, the central + feature of Coq. :ref:`writing-proofs` introduces this interactive + proof mode and the available proof languages. + :ref:`automatic-tactics` presents some more advanced tactics, while + :ref:`writing-tactics` is about the languages that allow a user to + combine tactics together and develop new ones. + +- **The third part shows how to use Coq in practice.** + :ref:`libraries` presents some of the essential reusable blocks from + the ecosystem and some particularly important extensions such as the + program extraction mechanism. :ref:`tools` documents important + tools that a user needs to build a Coq project. + +- In the appendix, :ref:`history-and-changes` presents the history of + Coq and changes in recent releases. This is an important reference + if you upgrade the version of Coq that you use. The various + :ref:`indexes <indexes>` are very useful to **quickly browse the + manual and find what you are looking for.** They are often the main + entry point to the manual. + +The full table of contents is presented below: diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 4beaff70f5..b0acd09af6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1200,45 +1200,47 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the ``universes(notemplate)`` + This can be prevented using the :attr:`universes(notemplate)` attribute. + Template polymorphism and full universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the latter is + enabled (through the :flag:`Universe Polymorphism` flag or the + :attr:`universes(polymorphic)` attribute) it will prevail over + automatic template polymorphism. + .. warn:: Automatically declaring @ident as template polymorphic. - Warning ``auto-template`` can be used to find which types are - implicitly declared template polymorphic by :flag:`Auto Template - Polymorphism`. + Warning ``auto-template`` can be used (it is off by default) to + find which types are implicitly declared template polymorphic by + :flag:`Auto Template Polymorphism`. An inductive type can be forced to be template polymorphic using - the ``universes(template)`` attribute: it should then fulfill the - criterion to be template polymorphic or an error is raised. - -.. exn:: Inductive @ident cannot be made template polymorphic. - - This error is raised when the `#[universes(template)]` attribute is - on but the inductive cannot be made polymorphic on any universe or be - inferred to live in :math:`\Prop` or :math:`\Set`. - - Template polymorphism and universe polymorphism (see Chapter - :ref:`polymorphicuniverses`) are incompatible, so if the later is - enabled it will prevail over automatic template polymorphism and - cause an error when using the ``universes(template)`` attribute. - -.. flag:: Template Check - - This flag is on by default. Turning it off disables the check of - locality of the sorts when abstracting the inductive over its - parameters. This is a deprecated and *unsafe* flag that can introduce - inconsistencies, it is only meant to help users incrementally update - code from Coq versions < 8.10 which did not implement this check. - The `Coq89.v` compatibility file sets this flag globally. A global - ``-no-template-check`` command line option is also available. Use at - your own risk. Use of this flag is recorded in the typing flags - associated to a definition but is *not* supported by the |Coq| - checker (`coqchk`). It will appear in :g:`Print Assumptions` and - :g:`About @ident` output involving inductive declarations that were - (potentially unsoundly) assumed to be template polymorphic. + the :attr:`universes(template)` attribute: in this case, the + warning is not emitted. + +.. attr:: universes(template) + + This attribute can be used to explicitly declare an inductive type + as template polymorphic, whether the :flag:`Auto Template + Polymorphism` flag is on or off. + + .. exn:: template and polymorphism not compatible + + This attribute cannot be used in a full universe polymorphic + context, i.e. if the :flag:`Universe Polymorphism` flag is on or + if the :attr:`universes(polymorphic)` attribute is used. + + .. exn:: Ill-formed template inductive declaration: not polymorphic on any universe. + + The attribute was used but the inductive definition does not + satisfy the criterion to be template polymorphic. + +.. attr:: universes(notemplate) + This attribute can be used to prevent an inductive type to be + template polymorphic, even if the :flag:`Auto Template + Polymorphism` flag is on. In practice, the rule **Ind-Family** is used by |Coq| only when all the inductive types of the inductive definition are declared with an arity diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst new file mode 100644 index 0000000000..07dcfff444 --- /dev/null +++ b/doc/sphinx/language/core/index.rst @@ -0,0 +1,37 @@ +.. _core-language: + +============= +Core language +============= + +At the heart of the Coq proof assistant is the Coq kernel. While +users have access to a language with many convenient features such as +notations, implicit arguments, etc. (that are presented in the +:ref:`next chapter <extensions>`), such complex terms get translated +down to a core language (the Calculus of Inductive Constructions) that +the kernel understands, and which we present here. Furthermore, while +users can build proofs interactively using tactics (see Chapter +:ref:`writing-proofs`), the role of these tactics is to incrementally +build a "proof term" which the kernel will verify. More precisely, a +proof term is a term of the Calculus of Inductive Constructions whose +type corresponds to a theorem statement. The kernel is a type checker +which verifies that terms have their expected type. + +This separation between the kernel on the one hand and the elaboration +engine and tactics on the other hand follows what is known as the "de +Bruijn criterion" (keeping a small and well delimited trusted code +base within a proof assistant which can be much more complex). This +separation makes it possible to reduce the trust in the whole system +to trusting a smaller, critical component: the kernel. In particular, +users may rely on external plugins that provide advanced and complex +tactics without fear of these tactics being buggy, because the kernel +will have to check their output. + +.. toctree:: + :maxdepth: 1 + + ../gallina-specification-language + ../cic + ../../addendum/universe-polymorphism + ../../addendum/sprop + ../module-system diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst new file mode 100644 index 0000000000..f22927d627 --- /dev/null +++ b/doc/sphinx/language/extensions/index.rst @@ -0,0 +1,26 @@ +.. _extensions: + +=================== +Language extensions +=================== + +Elaboration extends the language accepted by the Coq kernel to make it +easier to use. For example, this lets the user omit most type +annotations because they can be inferred, call functions with implicit +arguments which will be inferred as well, extend the syntax with +notations, factorize branches when pattern-matching, etc. In this +chapter, we present these language extensions and we give some +explanations on how this language is translated down to the core +language presented in the :ref:`previous chapter <core-language>`. + +.. toctree:: + :maxdepth: 1 + + ../gallina-extensions + ../../addendum/extended-pattern-matching + ../../user-extensions/syntax-extensions + ../../addendum/implicit-coercions + ../../addendum/type-classes + ../../addendum/canonical-structures + ../../addendum/program + ../../proof-engine/vernacular-commands diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index b9e181dd94..eff5eb60eb 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -42,9 +42,11 @@ expressions. In this sense, the :cmd:`Record` construction allows defining :cmd:`Record` and :cmd:`Structure` are synonyms. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: @@ -2053,12 +2055,15 @@ applied to an unknown structure instance (an implicit argument) and a 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 +.. cmd:: 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 - stops at the end of the :g:`Section` containig it. + structure (a record). + + This command supports the :attr:`local` attribute. When used, the + structure stops being a canonical instance at the end of the + :cmd:`Section` containing it. Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -2106,9 +2111,12 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. note:: - To prevent a field from being involved in the inference of canonical instances, - its declaration can be annotated with the :g:`#[canonical(false)]` attribute. + .. attr:: canonical(false) + + To prevent a field from being involved in the inference of + canonical instances, its declaration can be annotated with the + :attr:`canonical(false)` attribute (cf. the syntax of + :n:`@record_field`). .. example:: @@ -2121,11 +2129,17 @@ in :ref:`canonicalstructures`; here only a simple example is given. See :ref:`canonicalstructures` for a more realistic example. - .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the declaration :n:`Canonical @ident`. +.. attr:: 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. + .. cmd:: Print Canonical Projections {* @ident} This displays the list of global names that are components of some diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 4f0cf5f815..e710e19c12 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -767,6 +767,10 @@ Section :ref:`typing-rules`. If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified computation on :n:`@term`. + These commands also support the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`program` and + :attr:`canonical` attributes. + If :n:`@term` is omitted, Coq enters the proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant @@ -821,9 +825,11 @@ Inductive types may be impossible to derive (for example, when :n:`@ident` is a proposition). - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. @@ -851,9 +857,9 @@ Inductive types :n:`@ident` being defined (or :n:`@ident` applied to arguments in the case of annotated inductive types — cf. next section). -The following subsections show examples of simple inductive types, simple annotated -inductive types, simple parametric inductive types and mutually inductive -types. +The following subsections show examples of simple inductive types, +simple annotated inductive types, simple parametric inductive types, +mutually inductive types and private (matching) inductive types. .. _simple-inductive-types: @@ -1122,6 +1128,31 @@ Mutually defined inductive types A generic command :cmd:`Scheme` is useful to build automatically various mutual induction principles. +Private (matching) inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. attr:: private(matching) + + This attribute can be used to forbid the use of the :g:`match` + construct on objects of this inductive type outside of the module + where it is defined. There is also a legacy syntax using the + ``Private`` prefix (cf. :n:`@legacy_attr`). + + The main use case of private (matching) inductive types is to emulate + quotient types / higher-order inductive types in projects such as + the `HoTT library <https://github.com/HoTT/HoTT>`_. + +.. example:: + + .. coqtop:: all + + Module Foo. + #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat. + Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + End Foo. + Import Foo. + Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + Variants ~~~~~~~~ @@ -1132,9 +1163,11 @@ Variants be defined using :cmd:`Variant`). No induction scheme is generated for this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. .. exn:: The @num th argument of @ident must be @ident in @type. :undocumented: @@ -1160,9 +1193,11 @@ of the type. type, since such principles only make sense for inductive types. For co-inductive types, the only elimination principle is case analysis. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. .. example:: @@ -1607,14 +1642,21 @@ the proof and adds it to the environment. Attributes ----------- -.. insertprodn all_attrs legacy_attrs +.. insertprodn all_attrs legacy_attr .. prodn:: - all_attrs ::= {* #[ {*, @attr } ] } {? @legacy_attrs } + all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr } attr ::= @ident {? @attr_value } attr_value ::= = @string | ( {*, @attr } ) - legacy_attrs ::= {? {| Local | Global } } {? {| Polymorphic | Monomorphic } } {? Program } {? {| Cumulative | NonCumulative } } {? Private } + legacy_attr ::= Local + | Global + | Polymorphic + | Monomorphic + | Cumulative + | NonCumulative + | Private + | Program Attributes modify the behavior of a command or tactic. Syntactically, most commands and tactics can be decorated with attributes, but @@ -1623,7 +1665,7 @@ attributes not supported by the command or tactic will be flagged as errors. The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. -The legacy attributes (:n:`@legacy_attrs`) provide an older, alternate syntax +The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax for certain attributes. They are equivalent to new attributes as follows: ================ ================================ @@ -1633,65 +1675,12 @@ Legacy attribute New attribute `Global` :attr:`global` `Polymorphic` :attr:`universes(polymorphic)` `Monomorphic` :attr:`universes(monomorphic)` -`Cumulative` none -`NonCumulative` none -`Private` none +`Cumulative` :attr:`universes(cumulative)` +`NonCumulative` :attr:`universes(noncumulative)` +`Private` :attr:`private(matching)` `Program` :attr:`program` ================ ================================ -Some attributes are specific to a command, and so are described with -that command. Currently, the following attributes are recognized: - -.. attr:: universes(monomorphic) - :name: universes(monomorphic) - - See :ref:`polymorphicuniverses`. - -.. attr:: universes(polymorphic) - :name: universes(polymorphic) - - See :ref:`polymorphicuniverses`. - -.. attr:: universes(template) - :name: universes(template) - - See :ref:`Template-polymorphism` - -.. attr:: universes(notemplate) - :name: universes(notemplate) - - See :ref:`Template-polymorphism` - -.. attr:: program - - See :ref:`programs`. - -.. attr:: global - - See :ref:`controlling-locality-of-commands`. - -.. attr:: local - - See :ref:`controlling-locality-of-commands`. - -.. attr:: Cumulative - - Legacy attribute, only allowed in a polymorphic context. - Specifies that two instances of the same inductive type (family) are convertible - based on the universe variances; they do not need to be equal. - See :ref:`cumulative`. - -.. attr:: NonCumulative - - Legacy attribute, only allowed in a polymorphic context. - Specifies that two instances of the same inductive type (family) are convertible - only if all the universes are equal. - See :ref:`cumulative`. - -.. attr:: Private - - Legacy attribute. Documentation to be added. - .. attr:: deprecated ( {? since = @string , } {? note = @string } ) :name: deprecated @@ -1703,46 +1692,24 @@ that command. Currently, the following attributes are recognized: It can trigger the following warnings: - .. warn:: Tactic @qualid is deprecated since @string. @string. - :undocumented: - - .. warn:: Tactic Notation @qualid is deprecated since @string. @string. - :undocumented: - - .. warn:: Notation @string__1 is deprecated since @string__2. @string__3. - - :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, - :n:`@string__3` is the note. - -.. attr:: canonical + .. warn:: Tactic @qualid is deprecated since @string__since. @string__note. + Tactic Notation @qualid is deprecated since @string__since. @string__note. + Notation @string is deprecated since @string__since. @string__note. - 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 attribute 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:: + :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number, + :n:`@string__note` is the note (usually explains the replacement). - .. coqtop:: all reset warn + .. example:: - From Coq Require Program. - #[program] Definition one : nat := S _. - Next Obligation. - exact O. - Defined. + .. coqtop:: all reset warn - #[deprecated(since="8.9.0", note="Use idtac instead.")] - Ltac foo := idtac. + #[deprecated(since="8.9.0", note="Use idtac instead.")] + Ltac foo := idtac. - Goal True. - Proof. + Goal True. + Proof. now foo. - Abort. + Abort. .. warn:: Unsupported attribute diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst index 55c6d988f0..35837f8407 100644 --- a/doc/sphinx/license.rst +++ b/doc/sphinx/license.rst @@ -1,7 +1,7 @@ -License -------- +.. note:: **License** -This material (the Coq Reference Manual) may be distributed only subject to the -terms and conditions set forth in the Open Publication License, v1.0 or later -(the latest version is presently available at -http://www.opencontent.org/openpub). Options A and B are not elected. + This material (the Coq Reference Manual) may be distributed only + subject to the terms and conditions set forth in the Open + Publication License, v1.0 or later (the latest version is presently + available at http://www.opencontent.org/openpub). Options A and B + are not elected. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 98d222e317..aa4b6edd7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -227,7 +227,10 @@ and ``coqtop``, unless stated otherwise: type of the option. For flags ``Option Name`` is equivalent to ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` will enable :flag:`Universe Polymorphism`. Note that the quotes are - shell syntax, Coq does not see them. + shell syntax, Coq does not see them. Flags are processed after initialization + of the document. This includes the `Prelude` if loaded and any libraries loaded + through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom` + options. :-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 514353e39b..e5ff26520a 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -499,6 +499,40 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use (``.PHONY`` or not) please use ``CoqMakefile.local``. +Precompiling for ``native_compute`` ++++++++++++++++++++++++++++++++++++ + +To compile files for ``native_compute``, one can use the +``-native-compiler yes`` option of |Coq|, for instance by putting the +following in a :ref:`coqmakefilelocal` file: + +:: + + COQEXTRAFLAGS += -native-compiler yes + +The generated ``CoqMakefile`` installation target will then take care +of installing the extra ``.coq-native`` directories. + +.. note:: + + As an alternative to modifying any file, one can set the + environment variable when calling ``make``: + + :: + + COQEXTRAFLAGS="-native-compiler yes" make + + This can be useful when files cannot be modified, for instance when + installing via OPAM a package built with ``coq_makefile``: + + :: + + COQEXTRAFLAGS="-native-compiler yes" opam install coq-package + +.. note:: + + This requires all dependencies to be themselves compiled with + ``-native-compiler yes``. Building a |Coq| project with Dune ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 4401f8fa2f..895886605d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,34 +91,30 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? {| Local | Global | Export } } Set @flag +.. cmd:: Set @flag :name: Set - Sets :token:`flag` on. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` on. -.. cmd:: {? {| Local | Global | Export } } Unset @flag +.. cmd:: Unset @flag :name: Unset - Sets :token:`flag` off. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` off. .. cmd:: Test @flag Prints the current value of :token:`flag`. -.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } +.. cmd:: Set @option {| @num | @string } :name: Set @option - Sets :token:`option` to the specified value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to the specified value. -.. cmd:: {? {| Local | Global | Export } } Unset @option +.. cmd:: Unset @option :name: Unset @option - Sets :token:`option` to its default value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to its default value. .. cmd:: Test @option @@ -157,27 +153,37 @@ capital letter. A synonym for :cmd:`Print Options`. -.. _set_unset_scope_qualifiers: +Locality attributes supported by :cmd:`Set` and :cmd:`Unset` +```````````````````````````````````````````````````````````` + +The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, +:attr:`global` and :attr:`export` locality attributes: + +* no attribute: the original setting is *not* restored at the end of + the current module or section. +* :attr:`local` (an alternative syntax is to use the ``Local`` + prefix): the setting is applied within the current module or + section. The original value of the setting is restored at the end + of the current module or section. +* :attr:`export` (an alternative syntax is to use the ``Export`` + prefix): similar to :attr:`local`, the original value of the setting + is restored at the end of the current module or section. In + addition, if the value is set in a module, then :cmd:`Import`\-ing + the module sets the option or flag. +* :attr:`global` (an alternative syntax is to use the ``Global`` + prefix): the original setting is *not* restored at the end of the + current module or section. In addition, if the value is set in a + file, then :cmd:`Require`\-ing the file sets the option. + +Newly opened modules and sections inherit the current settings. -Scope qualifiers for :cmd:`Set` and :cmd:`Unset` -````````````````````````````````````````````````` - -:n:`{? {| Local | Global | Export } }` - -Flag and option settings can be global in scope or local to nested scopes created by -:cmd:`Module` and :cmd:`Section` commands. There are four alternatives: - -* no qualifier: the original setting is *not* restored at the end of the current module or section. -* **Local**: the setting is applied within the current scope. The original value of the option - or flag is restored at the end of the current module or section. -* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current - module or section. In addition, if the value is set in a file, then :cmd:`Require`-ing - the file sets the option. -* **Export**: similar to **Local**, the original value of the option or flag is restored at the - end of the current module or section. In addition, if the value is set in a file, then :cmd:`Import`-ing - the file sets the option. +.. note:: -Newly opened scopes inherit the current settings. + The use of the :attr:`global` attribute with the :cmd:`Set` and + :cmd:`Unset` commands is discouraged. If your goal is to define + project-wide settings, you should rather use the command-line + arguments ``-set`` and ``-unset`` for setting flags and options + (cf. :ref:`command-line-options`). .. _requests-to-the-environment: @@ -1152,49 +1158,51 @@ described first. Controlling the locality of commands ----------------------------------------- +.. attr:: global + local -.. cmd:: Local @command - Global @command - - Some commands support a Local or Global prefix modifier to control the - scope of their effect. There are four kinds of commands: - + Some commands support a :attr:`local` or :attr:`global` attribute + to control the scope of their effect. There is also a legacy (and + much more commonly used) syntax using the ``Local`` or ``Global`` + prefixes (see :n:`@legacy_attr`). There are four kinds of + commands: + Commands whose default is to extend their effect both outside the section and the module or library file they occur in. For these - commands, the Local modifier limits the effect of the command to the + commands, the :attr:`local` attribute limits the effect of the command to the current section or module it occurs in. As an example, the :cmd:`Coercion` and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the Local modifier limits the + library file they occur in. For these commands, the :attr:`local` attribute limits the effect of the command to the current module if the command does not occur in a - section and the Global modifier extends the effect outside the current + section and the :attr:`global` attribute extends the effect outside the current sections and current module if the command occurs in a section. As an example, the :cmd:`Arguments <Arguments (implicits)>`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the Global modifier is not + extension of their scope outside sections at all and the :attr:`global` attribute is not applicable to them. + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the ``Global`` - modifier extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` - (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + of the section or module they occur in. For these commands, the :attr:`global` + attribute extends their effect outside the sections and modules they + occur in. The :cmd:`Transparent` and :cmd:`Opaque` commands belong to this category. + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them. For these commands, the Local modifier - limits the effect to the current section or module while the Global - modifier extends the effect outside the module even when the command + when no section contains them. For these commands, the :attr:`local` attribute + limits the effect to the current section or module while the :attr:`global` + attribute extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. .. attr:: export - Some commands support an :attr:`export` attribute. The effect of the attribute - is to make the effect of the command available when the module containing it - is imported. The :cmd:`Hint` command accepts it for instance. + Some commands support an :attr:`export` attribute. The effect of + the attribute is to make the effect of the command available when + the module containing it is imported. It is supported in + particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` + commands. .. _controlling-typing-flags: diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst new file mode 100644 index 0000000000..a219770c69 --- /dev/null +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -0,0 +1,20 @@ +.. _automatic-tactics: + +===================================================== +Built-in decision procedures and programmable tactics +===================================================== + +Some tactics are largely automated and are able to solve complex +goals. This chapter presents both some decision procedures that can +be used to solve some specific categories of goals, and some +programmable tactics, that the user can instrument to handle some +complex goals in new domains. + +.. toctree:: + :maxdepth: 1 + + ../../addendum/omega + ../../addendum/micromega + ../../addendum/ring + ../../addendum/nsatz + ../../addendum/generalized-rewriting diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst new file mode 100644 index 0000000000..1af1b0b726 --- /dev/null +++ b/doc/sphinx/proofs/creating-tactics/index.rst @@ -0,0 +1,34 @@ +.. _writing-tactics: + +==================== +Creating new tactics +==================== + +The languages presented in this chapter allow one to build complex +tactics by combining existing ones with constructs such as +conditionals and looping. While :ref:`Ltac <ltac>` was initially +thought of as a language for doing some basic combinations, it has +been used successfully to build highly complex tactics as well, but +this has also highlighted its limits and fragility. The experimental +language :ref:`Ltac2 <ltac2>` is a typed and more principled variant +which is more adapted to building complex tactics. + +There are other solutions beyond these two tactic languages to write +new tactics: + +- `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin + which provides another typed tactic language. While Ltac2 belongs + to the ML language family, Mtac2 reuses the language of Coq itself + as the language to build Coq tactics. + +- The most traditional way of building new complex tactics is to write + a Coq plugin in OCaml. Beware that this also requires much more + effort and commitment. A tutorial for writing Coq plugins is + available in the Coq repository in `doc/plugin_tutorial + <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_. + +.. toctree:: + :maxdepth: 1 + + ../../proof-engine/ltac + ../../proof-engine/ltac2 diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst new file mode 100644 index 0000000000..a279a5957f --- /dev/null +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -0,0 +1,34 @@ +.. _writing-proofs: + +============== +Writing proofs +============== + +Coq is an interactive theorem prover, or proof assistant, which means +that proofs can be constructed interactively through a dialog between +the user and the assistant. The building blocks for this dialog are +tactics which the user will use to represent steps in the proof of a +theorem. + +Incomplete proofs have one or more open (unproven) sub-goals. Each +goal has its own context (a set of assumptions that can be used to +prove the goal). Tactics can transform goals and contexts. +Internally, the incomplete proof is represented as a partial proof +term, with holes for the unproven sub-goals. + +When a proof is complete, the user leaves the proof mode and defers +the verification of the resulting proof term to the :ref:`kernel +<core-language>`. + +This chapter is divided in several parts, describing the basic ideas +of the proof mode (during which tactics can be used), and several +flavors of tactics, including the SSReflect proof language. + +.. toctree:: + :maxdepth: 1 + + ../../proof-engine/proof-handling + ../../proof-engine/tactics + ../../proof-engine/ssreflect-proof-language + ../../proof-engine/detailed-tactic-examples + ../../user-extensions/proof-schemes diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst new file mode 100644 index 0000000000..d0848e6c3f --- /dev/null +++ b/doc/sphinx/using/libraries/index.rst @@ -0,0 +1,24 @@ +.. _libraries: + +===================== +Libraries and plugins +===================== + +Coq is distributed with a standard library and a set of internal +plugins (most of which provide tactics that have already been +presented in :ref:`writing-proofs`). This chapter presents this +standard library and some of these internal plugins which provide +features that are not tactics. + +In addition, Coq has a rich ecosystem of external libraries and +plugins. These libraries and plugins can be browsed online through +the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and +installed with the `opam package manager +<https://coq.inria.fr/opam-using.html>`_. + +.. toctree:: + :maxdepth: 1 + + ../../language/coq-library + ../../addendum/extraction + ../../addendum/miscellaneous-extensions diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst new file mode 100644 index 0000000000..4381c4d63d --- /dev/null +++ b/doc/sphinx/using/tools/index.rst @@ -0,0 +1,20 @@ +.. _tools: + +================================ +Command-line and graphical tools +================================ + +This chapter presents the command-line tools that users will need to +build their Coq project, the documentation of the CoqIDE standalone +user interface and the documentation of the parallel proof processing +feature that is supported by CoqIDE and several other user interfaces. +A list of available user interfaces to interact with Coq is available +on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. + +.. toctree:: + :maxdepth: 1 + + ../../practical-tools/coq-commands + ../../practical-tools/utilities + ../../practical-tools/coqide + ../../addendum/parallel-proof-processing diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 093c7a62b2..0b6ca5f178 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -13,6 +13,8 @@ (rule (targets html) + (alias stdlib-html) + (package coq-doc) (deps ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) @@ -31,6 +33,12 @@ (progn (cat %{header}) (cat index-list.html) (cat %{footer}))) (run cp _index.html html/index.html)))) -(alias - (name stdlib-html) - (deps html)) +; Installable directories are not yet fully supported by Dune. See +; ocaml/dune#1868. Yet, this makes coq-doc.install a valid target to +; generate the whole Coq documentation. And the result under +; _build/install/default/doc/coq-doc looks just right! + +(install + (files (html as html/stdlib)) + (section doc) + (package coq-doc)) diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index fe2e68a517..5bf122078d 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -140,10 +140,10 @@ field_ident: [ | "." ident ] -basequalid: [ -| REPLACE ident fields -| WITH ident LIST0 field_ident -| DELETE ident +qualid: [ | DELETENT ] + +qualid: [ +| ident LIST0 field_ident ] field: [ | DELETENT ] @@ -387,7 +387,7 @@ gallina: [ | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ] | DELETE assumptions_token inline assum_list -| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| REPLACE finite_token LIST1 inductive_definition SEP "with" | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) | "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) | "Variant" inductive_definition LIST0 ( "with" inductive_definition ) @@ -405,11 +405,6 @@ gallina: [ | WITH "Scheme" scheme LIST0 ( "with" scheme ) ] -DELETE: [ -| private_token -| cumulativity_token -] - constructor_list_or_record_decl: [ | OPTINREF ] @@ -737,12 +732,8 @@ assumption_token: [ | WITH [ "Variable" | "Variables" ] ] -legacy_attrs: [ -| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" -] - all_attrs: [ -| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs +| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr ] vernacular: [ @@ -842,7 +833,6 @@ SPLICE: [ | ne_lstring | ne_string | lstring -| basequalid | fullyqualid | global | reference diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 6897437457..2fabf92b7f 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -386,11 +386,6 @@ fullyqualid: [ | ident ] -basequalid: [ -| ident fields -| ident -] - name: [ | "_" | ident @@ -401,6 +396,10 @@ reference: [ | ident ] +qualid: [ +| reference +] + by_notation: [ | ne_string OPT [ "%" IDENT ] ] @@ -410,10 +409,6 @@ smart_global: [ | by_notation ] -qualid: [ -| basequalid -] - ne_string: [ | STRING ] @@ -436,7 +431,7 @@ lstring: [ integer: [ | NUMERAL -| "-" NUMERAL +| test_minus_nat "-" NUMERAL ] natural: [ @@ -735,21 +730,22 @@ attribute_value: [ | ] -vernac: [ -| "Local" vernac_poly -| "Global" vernac_poly -| vernac_poly +legacy_attr: [ +| "Local" +| "Global" +| "Polymorphic" +| "Monomorphic" +| "Cumulative" +| "NonCumulative" +| "Private" +| "Program" ] -vernac_poly: [ -| "Polymorphic" vernac_aux -| "Monomorphic" vernac_aux -| vernac_aux +vernac: [ +| LIST0 legacy_attr vernac_aux ] vernac_aux: [ -| "Program" gallina "." -| "Program" gallina_ext "." | gallina "." | gallina_ext "." | command "." @@ -774,7 +770,7 @@ gallina: [ | assumptions_token inline assum_list | def_token ident_decl def_body | "Let" identref def_body -| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| finite_token LIST1 inductive_definition SEP "with" | "Fixpoint" LIST1 rec_definition SEP "with" | "Let" "Fixpoint" LIST1 rec_definition SEP "with" | "CoFixpoint" LIST1 corec_definition SEP "with" @@ -903,16 +899,6 @@ finite_token: [ | "Class" ] -cumulativity_token: [ -| "Cumulative" -| "NonCumulative" -] - -private_token: [ -| "Private" -| -] - def_body: [ | binders ":=" reduce lconstr | binders ":" lconstr ":=" reduce lconstr diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index f26a174722..c3634466cc 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -172,7 +172,7 @@ vernacular: [ ] all_attrs: [ -| LIST0 ( "#[" LIST0 attr SEP "," "]" ) OPT legacy_attrs +| LIST0 ( "#[" LIST0 attr SEP "," "]" ) LIST0 legacy_attr ] attr: [ @@ -184,8 +184,15 @@ attr_value: [ | "(" LIST0 attr SEP "," ")" ] -legacy_attrs: [ -| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" +legacy_attr: [ +| "Local" +| "Global" +| "Polymorphic" +| "Monomorphic" +| "Cumulative" +| "NonCumulative" +| "Private" +| "Program" ] sort: [ @@ -338,20 +345,10 @@ pattern0: [ ] vernac: [ -| "Local" vernac_poly -| "Global" vernac_poly -| vernac_poly -] - -vernac_poly: [ -| "Polymorphic" vernac_aux -| "Monomorphic" vernac_aux -| vernac_aux +| LIST0 legacy_attr vernac_aux ] vernac_aux: [ -| "Program" gallina "." -| "Program" gallina_ext "." | gallina "." | gallina_ext "." | command "." |