diff options
Diffstat (limited to 'doc')
85 files changed, 838 insertions, 632 deletions
diff --git a/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst b/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst new file mode 100644 index 0000000000..c08ebb7f25 --- /dev/null +++ b/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Allow more inductive types in `Unset Positivity Checking` mode + (`#11811 <https://github.com/coq/coq/pull/11811>`_, + by SimonBoulier). diff --git a/doc/changelog/02-specification-language/10858-stuck-classed.md b/doc/changelog/02-specification-language/10858-stuck-classed.md new file mode 100644 index 0000000000..c7186f2c1d --- /dev/null +++ b/doc/changelog/02-specification-language/10858-stuck-classed.md @@ -0,0 +1,12 @@ +- **Changed:** + Typeclass resolution, accessible through :tacn:`typeclasses eauto`, + now suspends constraints according to their modes + instead of failing. If a typeclass constraint does not match + any of the declared modes for its class, the constraint is postponed, and + the proof search continues on other goals. Proof search does a fixed point + computation to try to solve them at a later stage of resolution. It does + not fail if there remain only stuck constraints at the end of resolution. + This makes typeclasses with declared modes more robust with respect to the + order of resolution. + (`#10858 <https://github.com/coq/coq/pull/10858>`_, + fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst index 32526babdb..633bb6731e 100644 --- a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst +++ b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst @@ -1,8 +1,8 @@ - **Added:** :cmd:`Arguments <Arguments (implicits)>` now supports setting - implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`. + implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}` (`#11098 <https://github.com/coq/coq/pull/11098>`_, by Hugo Herbelin, fixes `#4696 <https://github.com/coq/coq/pull/4696>`_, `#5173 <https://github.com/coq/coq/pull/5173>`_, `#9098 - <https://github.com/coq/coq/pull/9098>`_.). + <https://github.com/coq/coq/pull/9098>`_). diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst index a7ffde31fc..b0e658998b 100644 --- a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst +++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst @@ -1,6 +1,6 @@ - **Changed:** The warning raised when a trailing implicit is declared to be non maximally - inserted (with the command cmd:`Arguments <Arguments (implicits)>`) has been turned into an error. - This was deprecated since Coq 8.10. + inserted (with the command :cmd:`Arguments <Arguments (implicits)>`) has been turned into an error. + This was deprecated since Coq 8.10 (`#11368 <https://github.com/coq/coq/pull/11368>`_, by SimonBoulier). diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst index 3fa3f80301..b95bad2eb8 100644 --- a/doc/changelog/02-specification-language/11600-uniform-syntax.rst +++ b/doc/changelog/02-specification-language/11600-uniform-syntax.rst @@ -1,4 +1,5 @@ - **Added:** New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which parameters of an inductive are uniform. + See :ref:`parametrized-inductive-types` (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst index 5393fb3d8c..a8d4fc6ed2 100644 --- a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst +++ b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst @@ -1 +1,6 @@ -- Different interpretations in different scopes of the same notation string can now be associated to different printing formats; this fixes bug #6092 and #7766 (`#10832 <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin). +- **Fixed:** + Different interpretations in different scopes of the same notation + string can now be associated to different printing formats (`#10832 + <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin, + fixes `#6092 <https://github.com/coq/coq/issues/6092>`_ + and `#7766 <https://github.com/coq/coq/issues/7766>`_). diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst new file mode 100644 index 0000000000..1d30d16664 --- /dev/null +++ b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst @@ -0,0 +1,6 @@ +- **Added:** + Notations declared with the ``where`` clause in the declaration of + inductive types, coinductive types, record fields, fixpoints and + cofixpoints now support the ``only parsing`` modifier + (`#11602 <https://github.com/coq/coq/pull/11602>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11650-parensNew.rst b/doc/changelog/03-notations/11650-parensNew.rst index 5e2da594c6..f52a720428 100644 --- a/doc/changelog/03-notations/11650-parensNew.rst +++ b/doc/changelog/03-notations/11650-parensNew.rst @@ -1,4 +1,4 @@ - **Added:** - added option Set Printing Parentheses to print parentheses even when implied by associativity or precedence. + added the :flag:`Printing Parentheses` flag to print parentheses even when implied by associativity or precedence. (`#11650 <https://github.com/coq/coq/pull/11650>`_, by Hugo Herbelin and Abhishek Anand). diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst index eeae2ec519..32cd9b7135 100644 --- a/doc/changelog/04-tactics/10760-more-rapply.rst +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -4,5 +4,5 @@ rare cases where users were relying on :tacn:`rapply` inserting exactly 15 underscores and no more, due to the lemma having a completely unspecified codomain (and thus allowing for any number of - underscores), the tactic will now instead loop. (`#10760 - <https://github.com/coq/coq/pull/10760>`_, by Jason Gross) + underscores), the tactic will now instead loop (`#10760 + <https://github.com/coq/coq/pull/10760>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst index c72d085687..ba4d10590f 100644 --- a/doc/changelog/04-tactics/10998-zify-complements.rst +++ b/doc/changelog/04-tactics/10998-zify-complements.rst @@ -4,5 +4,5 @@ `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`. Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`) are also added to help users to declare new :tacn:`zify` class instances using - Micromega tactics. + Micromega tactics (`#10998 <https://github.com/coq/coq/pull/10998>`_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst index 2afa3990ac..e8cdfcca21 100644 --- a/doc/changelog/04-tactics/11023-nativecompute-timing.rst +++ b/doc/changelog/04-tactics/11023-nativecompute-timing.rst @@ -3,5 +3,5 @@ compiler) to emit separate timing information about compilation, execution, and reification. It replaces the timing information previously emitted when the `-debug` flag was set, and allows more - fine-grained timing of the native compiler. (`#11023 + fine-grained timing of the native compiler (`#11023 <https://github.com/coq/coq/pull/11023>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/11288-omega+depr.rst b/doc/changelog/04-tactics/11288-omega+depr.rst index 2832e6db61..3a2d421967 100644 --- a/doc/changelog/04-tactics/11288-omega+depr.rst +++ b/doc/changelog/04-tactics/11288-omega+depr.rst @@ -1,6 +1,6 @@ - **Removed:** The undocumented ``omega with`` tactic variant has been removed, - using ``lia`` is the recommended replacement, tho the old semantics - of ``omega with *`` can be recovered with ``zify; omega`` + using :tacn:`lia` is the recommended replacement, although the old semantics + of ``omega with *`` can also be recovered with ``zify; omega`` (`#11288 <https://github.com/coq/coq/pull/11288>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst index 5ecd46bced..79879c78d5 100644 --- a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst +++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst @@ -1,5 +1,5 @@ - **Fixed:** - Regression of ``lia`` due to more powerful ``zify`` + Regression of :tacn:`lia` due to more powerful :tacn:`zify` (`#11362 <https://github.com/coq/coq/pull/11362>`_, fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst index 4eb2732106..944dde99b8 100644 --- a/doc/changelog/04-tactics/11370-zify-elim-let.rst +++ b/doc/changelog/04-tactics/11370-zify-elim-let.rst @@ -1,3 +1,3 @@ -- **Changed** - Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml. +- **Changed:** + Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11429-zify-optimisation.rst b/doc/changelog/04-tactics/11429-zify-optimisation.rst new file mode 100644 index 0000000000..25927f9182 --- /dev/null +++ b/doc/changelog/04-tactics/11429-zify-optimisation.rst @@ -0,0 +1,3 @@ +- **Changed:** + Improve the efficiency of :tacn:`zify` by rewritting the remaining Ltac code in OCaml + (`#11429 <https://github.com/coq/coq/pull/11429>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst index 2a341261e5..52a2b2f0f6 100644 --- a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst +++ b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst @@ -1,9 +1,9 @@ - **Added:** - :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls. + :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls (`#11474 <https://github.com/coq/coq/pull/11474>`_, by Frédéric Besson). - **Fixed:** - Efficiency regression of ``lia`` + Efficiency regression of :tacn:`lia` (`#11474 <https://github.com/coq/coq/pull/11474>`_, fixes `#11436 <https://github.com/coq/coq/issues/11436>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst new file mode 100644 index 0000000000..3dd103b115 --- /dev/null +++ b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax :n:`pose proof (@ident:=@term)` as an + alternative to :n:`pose proof @term as @ident`, following the model of + :n:`pose (@ident:=@term)`. See documentation of :tacn:`pose proof` + (`#11522 <https://github.com/coq/coq/pull/11522>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/11760-firstorder-leaf.rst b/doc/changelog/04-tactics/11760-firstorder-leaf.rst new file mode 100644 index 0000000000..e6e4b827e5 --- /dev/null +++ b/doc/changelog/04-tactics/11760-firstorder-leaf.rst @@ -0,0 +1,9 @@ +- **Changed:** + The default tactic used by :g:`firstorder` is + :g:`auto with core` instead of :g:`auto with *`; + see :ref:`decisionprocedures` for details; + old behavior can be reset by using the `-compat 8.12` command-line flag; + to ease the migration of legacy code, the default solver can be set to `debug auto with *` + with `Set Firstorder Solver debug auto with *` + (`#11760 <https://github.com/coq/coq/pull/11760>`_, + by Vincent Laporte). diff --git a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst index 4acc423d10..e8233b9d13 100644 --- a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst +++ b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst @@ -1,4 +1,4 @@ - **Added:** - An array library for ltac2 (OCaml standard library compatible where possible). + An array library for Ltac2 (as compatible as possible with OCaml standard library) (`#10343 <https://github.com/coq/coq/pull/10343>`_, by Michael Soegtrop). diff --git a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst new file mode 100644 index 0000000000..5d3671bce1 --- /dev/null +++ b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst @@ -0,0 +1,4 @@ +- **Added:** + Ltac2 notations for :tacn:`enough` and :tacn:`eenough` + (`#11740 <https://github.com/coq/coq/pull/11740>`_, + by Michael Soegtrop). diff --git a/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst new file mode 100644 index 0000000000..b627fdbcc9 --- /dev/null +++ b/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + Deprecated the declaration of arbitrary terms as hints. Global + references are now preferred + (`#7791 <https://github.com/coq/coq/pull/7791>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst index e73be9c642..b263de017b 100644 --- a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst +++ b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst @@ -1,5 +1,5 @@ - **Changed:** - The :cmd:`Print Canonical Projections` command now can take constants and + The :cmd:`Print Canonical Projections` command can now take constants and prints only the unification rules that involve or are synthesized from given constants (`#10747 <https://github.com/coq/coq/pull/10747>`_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst index ec34c075ae..2bdc8052c6 100644 --- a/doc/changelog/07-commands-and-options/11164-let-cs.rst +++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst @@ -1,3 +1,3 @@ -- **Added:** A section variable introduces with :g:`Let` can be - declared as a :g:`Canonical Structure` (`#11164 +- **Added:** A section variable introduced with :cmd:`Let` can be + declared as a :cmd:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst b/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst new file mode 100644 index 0000000000..99f2d22d11 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst @@ -0,0 +1,9 @@ +- **Removed:** + Recursive OCaml loadpaths are not supported anymore; the command + ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the + preferred one. We have also dropped support for the non-qualified + version of the :cmd:`Add LoadPath` command, that is to say, + the ``Add LoadPath dir`` version; now, + you must always specify a prefix now using ``Add Loadpath dir as Prefix`` + (`#11618 <https://github.com/coq/coq/pull/11618>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst new file mode 100644 index 0000000000..5b0cdb5914 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst @@ -0,0 +1,5 @@ +- **Added:** + Several commands (`Search`, `About`, ...) now print the implicit arguments + in brackets when printing types. + (`#11795 <https://github.com/coq/coq/pull/11795>`_, + by SimonBoulier). diff --git a/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst new file mode 100644 index 0000000000..9341eebb58 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst @@ -0,0 +1,5 @@ +- **Added:** + the :cmd:`Hint` commands now accept the :attr:`export` locality as + an attribute, allowing to make import-scoped hints + (`#11812 <https://github.com/coq/coq/pull/11812>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst b/doc/changelog/08-tools/11409-mltop+deprecate_use.rst index db433ad64c..f4f110ed67 100644 --- a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst +++ b/doc/changelog/08-tools/11409-mltop+deprecate_use.rst @@ -1,5 +1,5 @@ - **Removed:** The `-load-ml-source` and `-load-ml-object` command line options have been removed; their use was very limited, you can achieve the same adding - additional object files in the linking step or using a plugin. + additional object files in the linking step or using a plugin (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst index 32a4750b73..3f93d60926 100644 --- a/doc/changelog/08-tools/11523-coqdep+refactor2.rst +++ b/doc/changelog/08-tools/11523-coqdep+refactor2.rst @@ -4,7 +4,7 @@ files are not supported as input. Also, several deprecated options have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``, ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will - not load any path by default now, ``-R/-Q`` should be used instead. + not load any path by default now, ``-R/-Q`` should be used instead (`#11523 <https://github.com/coq/coq/pull/11523>`_ and `#11589 <https://github.com/coq/coq/pull/11589>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst b/doc/changelog/08-tools/11617-toplevel+boot.rst index 49dd0ee2d8..49dd0ee2d8 100644 --- a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst +++ b/doc/changelog/08-tools/11617-toplevel+boot.rst diff --git a/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst b/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst index 99b1592fb3..cbd97688c3 100644 --- a/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst +++ b/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst @@ -1,4 +1,4 @@ - **Fixed:** - Fix file paths containing spaces when compiling + Compiling file paths containing spaces (`#10008 <https://github.com/coq/coq/pull/10008>`_, by snyke7, fixing `#11595 <https://github.com/coq/coq/pull/11595>`_). diff --git a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst index 6294cdb24a..49ac16eee9 100644 --- a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst +++ b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst @@ -1,4 +1,4 @@ - **Removed:** - Removed the "Tactic" menu from CoqIDE which had been unmaintained for a number of years + "Tactic" menu from CoqIDE which had been unmaintained for a number of years (`#11414 <https://github.com/coq/coq/pull/11414>`_, by Pierre-Marie Pédrot). diff --git a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst index cb92945b8b..9d22a858f1 100644 --- a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst +++ b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst @@ -1,4 +1,4 @@ - **Removed:** - Removed the "Revert all buffers" command from CoqIDE which had been broken for a long time + "Revert all buffers" command from CoqIDE which had been broken for a long time (`#11415 <https://github.com/coq/coq/pull/11415>`_, by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/11127-trunk.rst b/doc/changelog/10-standard-library/11127-trunk.rst index ef1d41d17f..3f461397ae 100644 --- a/doc/changelog/10-standard-library/11127-trunk.rst +++ b/doc/changelog/10-standard-library/11127-trunk.rst @@ -1,2 +1,2 @@ -- **Added:** theorem :g:`bezout_comm` for natural numbers +- **Added:** Theorem :g:`bezout_comm` for natural numbers (`#11127 <https://github.com/coq/coq/pull/11127>`_, by Daniel de Rauglaudre). diff --git a/doc/changelog/03-notations/11240-rew-dependent.rst b/doc/changelog/10-standard-library/11240-rew-dependent.rst index e9daab0c2c..e9daab0c2c 100644 --- a/doc/changelog/03-notations/11240-rew-dependent.rst +++ b/doc/changelog/10-standard-library/11240-rew-dependent.rst diff --git a/doc/changelog/10-standard-library/11686-fix-int-notations.rst b/doc/changelog/10-standard-library/11686-fix-int-notations.rst index cc820c5a25..4959a9f9b1 100644 --- a/doc/changelog/10-standard-library/11686-fix-int-notations.rst +++ b/doc/changelog/10-standard-library/11686-fix-int-notations.rst @@ -2,5 +2,5 @@ Notations :n:`[|@term|]` and :n:`[||@term||]` for morphisms from 63-bit integers to :g:`Z` and :g:`zn2z int` have been removed in favor of :n:`φ(@term)` and :n:`Φ(@term)` respectively. These notations were - breaking Ltac parsing. (`#11686 <https://github.com/coq/coq/pull/11686>`_, + breaking Ltac parsing (`#11686 <https://github.com/coq/coq/pull/11686>`_, by Maxime Dénès). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst b/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst index 03c2ccc1d2..dc76178e0d 100644 --- a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst +++ b/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst @@ -1,4 +1,4 @@ - **Removed:** - Python 2 is not longer required in any part of the codebase. + Python 2 is not longer required in any part of the codebase (`#11245 <https://github.com/coq/coq/pull/11245>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst b/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst new file mode 100644 index 0000000000..94e2c34828 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst @@ -0,0 +1,4 @@ +- **Added:** + Bump official OCaml support to 4.09.1 + (`#11860 <https://github.com/coq/coq/pull/11860>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst index c6778403d4..0636e303c4 100644 --- a/doc/changelog/12-misc/10486-native-string-extraction.rst +++ b/doc/changelog/12-misc/10486-native-string-extraction.rst @@ -2,6 +2,6 @@ Support for better extraction of strings in OCaml and Haskell: `ExtOcamlNativeString` provides bindings from the Coq `String` type to the OCaml `string` type, and string literals can be extracted to literals, - both in OCaml and Haskell. (`#10486 + both in OCaml and Haskell (`#10486 <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from Maxime Dénès, review by Hugo Herbelin). @@ -14,7 +14,7 @@ unreleased.rst (env_var SPHINXWARNOPT)) (action - (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 89b4bda71a..0802b5d0b4 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -3,8 +3,8 @@ ============================= .. - README.rst is auto-generated from README.template.rst and the coqrst docs; - use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + README.rst is auto-generated from README.template.rst and the coqrst/*.py files + (in particular coqdomain.py). Use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. @@ -97,7 +97,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica ``.. cmd::`` :black_nib: A Coq command. Example:: - .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident } + .. cmd:: Infix @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @ident } This command is equivalent to :n:`…`. diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index c5e0007e78..5762967c36 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -3,8 +3,8 @@ ============================= .. - README.rst is auto-generated from README.template.rst and the coqrst docs; - use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + README.rst is auto-generated from README.template.rst and the coqrst/*.py files + (in particular coqdomain.py). Use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. diff --git a/doc/sphinx/_static/ansi-dark.css b/doc/sphinx/_static/ansi-dark.css index bbace7c553..f02f522bdd 100644 --- a/doc/sphinx/_static/ansi-dark.css +++ b/doc/sphinx/_static/ansi-dark.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index b3b5341166..2a618f68d2 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/coqdoc.css b/doc/sphinx/_static/coqdoc.css index 7a3d59d4c0..32cb0a7a15 100644 --- a/doc/sphinx/_static/coqdoc.css +++ b/doc/sphinx/_static/coqdoc.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index 3806ba6ee6..733a73bd21 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/notations.js b/doc/sphinx/_static/notations.js index 63112312d0..d2eee1f5fa 100644 --- a/doc/sphinx/_static/notations.js +++ b/doc/sphinx/_static/notations.js @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/_static/pre-text.css b/doc/sphinx/_static/pre-text.css index 9d133fb1aa..aa4180d246 100644 --- a/doc/sphinx/_static/pre-text.css +++ b/doc/sphinx/_static/pre-text.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 15f42591ce..8ec51e45ba 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -5,8 +5,6 @@ Extended pattern matching :Authors: Cristina Cornes and Hugo Herbelin -.. TODO links to figures - This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides @@ -14,7 +12,7 @@ This section describes the full form of pattern matching in |Coq| terms. Patterns -------- -The full syntax of match is presented in Figures 1.1 and 1.2. +The full syntax of :g:`match` is presented in section :ref:`term`. Identifiers in patterns are either constructor names or variables. Any identifier that is not the constructor of an inductive or co-inductive type is considered to be a variable. A variable name cannot occur more @@ -496,9 +494,8 @@ We can use multiple patterns to write the proof of the lemma In the example of :g:`dec`, the first match is dependent while the second is not. -The user can also use match in combination with the tactic :tacn:`refine` (see -Section 8.2.3) to build incomplete proofs beginning with a match -construction. +The user can also use match in combination with the tactic :tacn:`refine` +to build incomplete proofs beginning with a :g:`match` construction. Pattern-matching on inductive objects involving local definitions diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 94ab6e789c..315c9d4a80 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -713,48 +713,119 @@ Definitions ~~~~~~~~~~~ The generalized rewriting tactic is based on a set of strategies that can be -combined to obtain custom rewriting procedures. Its set of strategies is based +combined to create custom rewriting procedures. Its set of strategies is based on the programmable rewriting strategies with generic traversals by Visser et al. :cite:`Luttik97specificationof` :cite:`Visser98`, which formed the core of the Stratego transformation language :cite:`Visser01`. Rewriting strategies -are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a -strategy expression. Strategies are defined inductively as described by the -following grammar: - -.. productionlist:: coq - strategy : `qualid` (lemma, left to right) - : <- `qualid` (lemma, right to left) - : fail (failure) - : id (identity) - : refl (reflexivity) - : progress `strategy` (progress) - : try `strategy` (try catch) - : `strategy` ; `strategy` (composition) - : choice `strategy` `strategy` (left_biased_choice) - : repeat `strategy` (one or more) - : any `strategy` (zero or more) - : subterm `strategy` (one subterm) - : subterms `strategy` (all subterms) - : innermost `strategy` (innermost first) - : outermost `strategy` (outermost first) - : bottomup `strategy` (bottom-up) - : topdown `strategy` (top-down) - : hints `ident` (apply hints from hint database) - : terms `term` ... `term` (any of the terms) - : eval `red_expr` (apply reduction) - : fold `term` (unify) - : ( `strategy` ) - -Actually a few of these are defined in term of the others using a +are applied using the tactic :n:`rewrite_strat @rewstrategy`. + +.. insertprodn rewstrategy rewstrategy + +.. prodn:: + rewstrategy ::= @one_term + | <- @one_term + | fail + | id + | refl + | progress @rewstrategy + | try @rewstrategy + | @rewstrategy ; @rewstrategy + | choice @rewstrategy @rewstrategy + | repeat @rewstrategy + | any @rewstrategy + | subterm @rewstrategy + | subterms @rewstrategy + | innermost @rewstrategy + | outermost @rewstrategy + | bottomup @rewstrategy + | topdown @rewstrategy + | hints @ident + | terms {* @one_term } + | eval @red_expr + | fold @one_term + | ( @rewstrategy ) + | old_hints @ident + +:n:`@one_term` + lemma, left to right + +:n:`<- @one_term` + lemma, right to left + +:n:`fail` + failure + +:n:`id` + identity + +:n:`refl` + reflexivity + +:n:`progress @rewstrategy` + progress + +:n:`try @rewstrategy` + try catch + +:n:`@rewstrategy ; @rewstrategy` + composition + +:n:`choice @rewstrategy @rewstrategy` + left_biased_choice + +:n:`repeat @rewstrategy` + one or more + +:n:`any @rewstrategy` + zero or more + +:n:`subterm @rewstrategy` + one subterm + +:n:`subterms @rewstrategy` + all subterms + +:n:`innermost @rewstrategy` + innermost first + +:n:`outermost @rewstrategy` + outermost first + +:n:`bottomup @rewstrategy` + bottom-up + +:n:`topdown @rewstrategy` + top-down + +:n:`hints @ident` + apply hints from hint database + +:n:`terms {* @one_term }` + any of the terms + +:n:`eval @red_expr` + apply reduction + +:n:`fold @term` + unify + +:n:`( @rewstrategy )` + to be documented + +:n:`old_hints @ident` + to be documented + + +A few of these are defined in terms of the others using a primitive fixpoint operator: -- :n:`try @strategy := choice @strategy id` -- :n:`any @strategy := fix @ident. try (@strategy ; @ident)` -- :n:`repeat @strategy := @strategy; any @strategy` -- :n:`bottomup @strategy := fix @ident. (choice (progress (subterms @ident)) @strategy) ; try @ident` -- :n:`topdown @strategy := fix @ident. (choice @strategy (progress (subterms @ident))) ; try @ident` -- :n:`innermost @strategy := fix @ident. (choice (subterm @ident) @strategy)` -- :n:`outermost @strategy := fix @ident. (choice @strategy (subterm @ident))` +- :n:`try @rewstrategy := choice @rewstrategy id` +- :n:`any @rewstrategy := fix @ident. try (@rewstrategy ; @ident)` +- :n:`repeat @rewstrategy := @rewstrategy; any @rewstrategy` +- :n:`bottomup @rewstrategy := fix @ident. (choice (progress (subterms @ident)) @rewstrategy) ; try @ident` +- :n:`topdown @rewstrategy := fix @ident. (choice @rewstrategy (progress (subterms @ident))) ; try @ident` +- :n:`innermost @rewstrategy := fix @ident. (choice (subterm @ident) @rewstrategy)` +- :n:`outermost @rewstrategy := fix @ident. (choice @rewstrategy (subterm @ident))` The basic control strategy semantics are straightforward: strategies are applied to subterms of the term to rewrite, starting from the root @@ -764,18 +835,18 @@ hand-side. Composition can be used to continue rewriting on the current subterm. The ``fail`` strategy always fails while the identity strategy succeeds without making progress. The reflexivity strategy succeeds, making progress using a reflexivity proof of rewriting. -``progress`` tests progress of the argument :token:`strategy` and fails if no +``progress`` tests progress of the argument :n:`@rewstrategy` and fails if no progress was made, while ``try`` always succeeds, catching failures. ``choice`` is left-biased: it will launch the first strategy and fall back on the second one in case of failure. One can iterate a strategy at least 1 time using ``repeat`` and at least 0 times using ``any``. -The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to +The ``subterm`` and ``subterms`` strategies apply their argument :n:`@rewstrategy` to respectively one or all subterms of the current term under consideration, left-to-right. ``subterm`` stops at the first subterm for -which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost`` +which :n:`@rewstrategy` made progress. The composite strategies ``innermost`` and ``outermost`` perform a single innermost or outermost rewrite using their argument -:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many +:n:`@rewstrategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. @@ -793,7 +864,7 @@ Usage ~~~~~ -.. tacn:: rewrite_strat @strategy {? in @ident } +.. tacn:: rewrite_strat @rewstrategy {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index b007509b2e..1f33775a01 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,12 +37,13 @@ In addition to these user-defined classes, we have two built-in classes: * ``Funclass``, the class of functions; its objects are all the terms with a functional type, i.e. of form :g:`forall x:A,B`. -Formally, the syntax of classes is defined as: + .. insertprodn class class + + .. prodn:: + class ::= Funclass + | Sortclass + | @smart_qualid -.. productionlist:: - class: `qualid` - : Sortclass - : Funclass Coercions @@ -186,37 +187,12 @@ Declaring Coercions This defines :token:`ident` just like :n:`Let @ident := @term {? @type }`, and then declares :token:`ident` as a coercion between it source and its target. -Assumptions can be declared as coercions at declaration time. -This extends the grammar of assumptions from -Figure :ref:`vernacular` as follows: - -.. - FIXME: - \comindex{Variable \mbox{\rm (and coercions)}} - \comindex{Axiom \mbox{\rm (and coercions)}} - \comindex{Parameter \mbox{\rm (and coercions)}} - \comindex{Hypothesis \mbox{\rm (and coercions)}} - -.. productionlist:: - assumption : `assumption_token` `assums` . - assums : `simple_assums` - : (`simple_assums`) ... (`simple_assums`) - simple_assums : `ident` ... `ident` :[>] `term` - -If the extra ``>`` is present before the type of some assumptions, these -assumptions are declared as coercions. - -Similarly, constructors of inductive types can be declared as coercions at -definition time of the inductive type. This extends and modifies the -grammar of inductive types from Figure :ref:`vernacular` as follows: - -.. - FIXME: - \comindex{Inductive \mbox{\rm (and coercions)}} - \comindex{CoInductive \mbox{\rm (and coercions)}} - -Especially, if the extra ``>`` is present in a constructor -declaration, this constructor is declared as a coercion. +Some objects can be declared as coercions when they are defined. +This applies to :ref:`assumptions<gallina-assumptions>` and +constructors of :ref:`inductive types and record fields<gallina-inductive-definitions>`. +Use :n:`:>` instead of :n:`:` before the +:n:`@type` of the assumption to do so. See :n:`@of_type`. + .. cmd:: Identity Coercion @ident : @class >-> @class diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 1098aa75da..76174e32b5 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -300,70 +300,79 @@ following property: The syntax for adding a new ring is -.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )} - - The :token:`ident` is not relevant. It is used just for error messages. The - :token:`term` is a proof that the ring signature satisfies the (semi-)ring +.. cmd:: Add Ring @ident : @one_term {? ( {+, @ring_mod } ) } + + .. insertprodn ring_mod ring_mod + + .. prodn:: + ring_mod ::= decidable @one_term + | abstract + | morphism @one_term + | constants [ @ltac_expr ] + | preprocess [ @ltac_expr ] + | postprocess [ @ltac_expr ] + | setoid @one_term @one_term + | sign @one_term + | power @one_term [ {+ @qualid } ] + | power_tac @one_term [ @ltac_expr ] + | div @one_term + | closed [ {+ @qualid } ] + + The :n:`@ident` is used only for error messages. The + :n:`@one_term` is a proof that the ring signature satisfies the (semi-)ring axioms. The optional list of modifiers is used to tailor the behavior - of the tactic. The following list describes their syntax and effects: - - .. productionlist:: coq - ring_mod : abstract | decidable `term` | morphism `term` - : setoid `term` `term` - : constants [ `tactic` ] - : preprocess [ `tactic` ] - : postprocess [ `tactic` ] - : power_tac `term` [ `tactic` ] - : sign `term` - : div `term` - - abstract + of the tactic. Here are their effects: + + :n:`abstract` declares the ring as abstract. This is the default. - decidable :n:`@term` + :n:`decidable @one_term` declares the ring as computational. The expression - :n:`@term` is the correctness proof of an equality test ``?=!`` + :n:`@one_term` is the correctness proof of an equality test ``?=!`` (which should be evaluable). Its type should be of the form ``forall x y, x ?=! y = true → x == y``. - morphism :n:`@term` + :n:`morphism @one_term` declares the ring as a customized one. The expression - :n:`@term` is a proof that there exists a morphism between a set of + :n:`@one_term` is a proof that there exists a morphism between a set of coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and ``Ring_theory.semi_morph``). - setoid :n:`@term` :n:`@term` + :n:`setoid @one_term @one_term` forces the use of given setoid. The first - :n:`@term` is a proof that the equality is indeed a setoid (see - ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the + :n:`@one_term` is a proof that the equality is indeed a setoid (see + ``Setoid.Setoid_Theory``), and the second a proof that the ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and ``Ring_theory.sring_eq_ext``). This modifier needs not be used if the setoid and morphisms have been declared. - constants [ :n:`@tactic` ] - specifies a tactic expression :n:`@tactic` that, given a + :n:`constants [ @ltac_expr ]` + specifies a tactic expression :n:`@ltac_expr` that, given a term, returns either an object of the coefficient set that is mapped to the expression via the morphism, or returns ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 to their counterpart in the coefficient set. This is generally not desirable for non trivial computational rings. - preprocess [ :n:`@tactic` ] - specifies a tactic :n:`@tactic` that is applied as a + :n:`preprocess [ @ltac_expr ]` + specifies a tactic :n:`@ltac_expr` that is applied as a preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to transform a goal so that it is better recognized. For instance, ``S n`` can be changed to ``plus 1 n``. - postprocess [ :n:`@tactic` ] - specifies a tactic :n:`@tactic` that is applied as a final + :n:`postprocess [ @ltac_expr ]` + specifies a tactic :n:`@ltac_expr` that is applied as a final step for :tacn:`ring_simplify`. For instance, it can be used to undo modifications of the preprocessor. - power_tac :n:`@term` [ :n:`@tactic` ] + :n:`power @one_term [ {+ @qualid } ]` + to be documented + + :n:`power_tac @one_term @ltac_expr ]` allows :tacn:`ring` and :tacn:`ring_simplify` to recognize power expressions with a constant positive integer exponent (example: - :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies + :math:`x^2` ). The term :n:`@one_term` is a proof that a given power function satisfies the specification of a power function (term has to be a proof of ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression that, given a term, “abstracts” it into an object of type |N| whose @@ -374,22 +383,25 @@ The syntax for adding a new ring is and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic does not recognize power expressions as ring expressions. - sign :n:`@term` + :n:`sign @one_term` allows :tacn:`ring_simplify` to use a minus operation when outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The term :token:`term` is a proof that a given sign function indicates expressions that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. - div :n:`@term` + :n:`div @one_term` allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with - coefficients other than 1 in the rewriting. The term :n:`@term` is a proof + coefficients other than 1 in the rewriting. The term :n:`@one_term` is a proof that a given division function satisfies the specification of an - euclidean division function (:n:`@term` has to be a proof of + euclidean division function (:n:`@one_term` has to be a proof of ``Ring_theory.div_theory``). For example, this function is called when trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + :n:`closed [ {+ @qualid } ]` + to be documented + Error messages: .. exn:: Bad ring structure. @@ -653,24 +665,27 @@ zero for the correctness of the algorithm. The syntax for adding a new field is -.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )} +.. cmd:: Add Field @ident : @one_term {? ( {+, @field_mod } ) } - The :n:`@ident` is not relevant. It is used just for error - messages. :n:`@term` is a proof that the field signature satisfies the + .. insertprodn field_mod field_mod + + .. prodn:: + field_mod ::= @ring_mod + | completeness @one_term + + The :n:`@ident` is used only for error + messages. :n:`@one_term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. - .. productionlist:: coq - field_mod : `ring_mod` | completeness `term` - Since field tactics are built upon ``ring`` - tactics, all modifiers of the ``Add Ring`` apply. There is only one + tactics, all modifiers of :cmd:`Add Ring` apply. There is only one specific modifier: - completeness :n:`@term` + completeness :n:`@one_term` allows the field tactic to prove automatically that the image of nonzero coefficients are mapped to nonzero - elements of the field. :n:`@term` is a proof of + elements of the field. :n:`@one_term` is a proof of :g:`forall x y, [x] == [y] -> x ?=! y = true`, which is the completeness of equality on coefficients w.r.t. the field equality. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index af4e9051bb..7abeca7815 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -385,8 +385,10 @@ few other commands related to typeclasses. .. tacn:: typeclasses eauto :name: typeclasses eauto - This tactic uses a different resolution engine than :tacn:`eauto` and - :tacn:`auto`. The main differences are the following: + This proof search tactic implements the resolution engine that is run + implicitly during type-checking. This tactic uses a different resolution + engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the + following: + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in the new proof engine (as of Coq 8.6), meaning that backtracking is @@ -422,6 +424,17 @@ few other commands related to typeclasses. resolution with the local hypotheses use full conversion during unification. + + The mode hints (see :cmd:`Hint Mode`) associated to a class are + taken into account by :tacn:`typeclasses eauto`. When a goal + does not match any of the declared modes for its head (if any), + instead of failing like :tacn:`eauto`, the goal is suspended and + resolution proceeds on the remaining goals. + If after one run of resolution, there remains suspended goals, + resolution is launched against on them, until it reaches a fixed + point when the set of remaining suspended goals does not change. + Using `solve [typeclasses eauto]` can be used to ensure that + no suspended goals remain. + + When considering local hypotheses, we use the union of all the modes declared in the given databases. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index c069782add..0e326f45d2 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -372,16 +372,11 @@ to universes and explicitly instantiate polymorphic definitions. universe quantification will be discharged on each section definition independently. -.. cmd:: Constraint @universe_constraint - Polymorphic Constraint @universe_constraint +.. cmd:: Constraint @univ_constraint + Polymorphic Constraint @univ_constraint This command declares a new constraint between named universes. - .. productionlist:: coq - universe_constraint : `qualid` < `qualid` - : `qualid` <= `qualid` - : `qualid` = `qualid` - 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 diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 22102aa3ab..98272810f6 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -1,8 +1,8 @@ #!/usr/bin/env python3 ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## @@ -183,9 +183,9 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ + 'assums', 'binders', 'collection', - 'command', 'definition', 'dirpath', 'inductive', @@ -194,7 +194,6 @@ nitpick_ignore = [ ('token', token) for token in [ 'module', 'simple_tactic', 'symbol', - 'tactic', 'term_pattern', 'term_pattern_string', 'toplevel_selector', diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css index 2ac2af1c13..a325a33842 100644 --- a/doc/sphinx/coqdoc.css +++ b/doc/sphinx/coqdoc.css @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 6c1d83b3b8..b9e181dd94 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -24,7 +24,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. - field : `ident` [ `binders` ] : `type` [ where `notation` ] + field : `ident` [ `binders` ] : `type` [ `decl_notations` ] : `ident` [ `binders` ] [: `type` ] := `term` .. cmd:: {| Record | Structure } @inductive_definition {* with @inductive_definition } @@ -35,8 +35,10 @@ expressions. In this sense, the :cmd:`Record` construction allows defining the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of fields. For a given field :token:`ident`, its type is :n:`forall {* @binder }, @type`. - Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the - order of the fields is important. Finally, :token:`binders` are parameters of the record. + Notice that the type of a particular identifier may depend on a previously-given identifier. Thus the + order of the fields is important. The record can depend as a whole on parameters :token:`binders` + and each field can also depend on its own :token:`binders`. Finally, notations can be attached to + fields using the :n:`decl_notations` annotation. :cmd:`Record` and :cmd:`Structure` are synonyms. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index e12ff1ba98..4f0cf5f815 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -158,6 +158,8 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. | @term1 arg ::= ( @ident := @term ) | @term1 + one_term ::= @term1 + | @ @qualid {? @univ_annot } term1 ::= @term_projection | @term0 % @ident | @term0 @@ -175,6 +177,13 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. | ltac : ( @ltac_expr ) field_def ::= @qualid {* @binder } := @term +.. note:: + + Many commands and tactics use :n:`@one_term` rather than :n:`@term`. + The former need to be enclosed in parentheses unless they're very + simple, such as a single identifier. This avoids confusing a space-separated + list of terms with a :n:`@term1` applied to a list of arguments. + .. _types: Types @@ -591,17 +600,15 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). Recursive and co-recursive functions: fix and cofix --------------------------------------------------- -.. insertprodn term_fix term1_extended +.. insertprodn term_fix fixannot .. prodn:: term_fix ::= let fix @fix_body in @term | fix @fix_body {? {+ with @fix_body } for @ident } fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term fixannot ::= %{ struct @ident %} - | %{ wf @term1_extended @ident %} - | %{ measure @term1_extended {? @ident } {? @term1_extended } %} - term1_extended ::= @term1 - | @ @qualid {? @univ_annot } + | %{ wf @one_term @ident %} + | %{ measure @one_term {? @ident } {? @one_term } %} The expression ":n:`fix @ident__1 @binder__1 : @type__1 := @term__1 with … with @ident__n @binder__n : @type__n := @term__n for @ident__i`" denotes the @@ -1472,11 +1479,11 @@ Computations | vm_compute {? @ref_or_pattern_occ } | native_compute {? @ref_or_pattern_occ } | unfold {+, @unfold_occ } - | fold {+ @term1_extended } + | fold {+ @one_term } | pattern {+, @pattern_occ } | @ident - delta_flag ::= {? - } [ {+ @smart_global } ] - smart_global ::= @qualid + delta_flag ::= {? - } [ {+ @smart_qualid } ] + smart_qualid ::= @qualid | @by_notation by_notation ::= @string {? % @ident } strategy_flag ::= {+ @red_flags } @@ -1488,16 +1495,16 @@ Computations | cofix | zeta | delta {? @delta_flag } - ref_or_pattern_occ ::= @smart_global {? at @occs_nums } - | @term1_extended {? at @occs_nums } + ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums } + | @one_term {? at @occs_nums } occs_nums ::= {+ @num_or_var } | - @num_or_var {* @int_or_var } num_or_var ::= @num | @ident int_or_var ::= @int | @ident - unfold_occ ::= @smart_global {? at @occs_nums } - pattern_occ ::= @term1_extended {? at @occs_nums } + unfold_occ ::= @smart_qualid {? at @occs_nums } + pattern_occ ::= @one_term {? at @occs_nums } See :ref:`Conversion-rules`. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 179dff9959..514353e39b 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -505,34 +505,41 @@ Building a |Coq| project with Dune .. note:: + Dune's Coq support is still experimental; we strongly recommend + using Dune 2.3 or later. + +.. note:: + The canonical documentation for the Coq Dune extension is maintained upstream; please refer to the `Dune manual - <https://dune.readthedocs.io/>`_ for up-to-date information. + <https://dune.readthedocs.io/>`_ for up-to-date information. This + documentation is up to date for Dune 2.3. Building a Coq project with Dune requires setting up a Dune project for your files. This involves adding a ``dune-project`` and -``pkg.opam`` file to the root (``pkg.opam`` can be empty), and then -providing ``dune`` files in the directories your ``.v`` files are -placed. For the experimental version "0.1" of the Coq Dune language, -|Coq| library stanzas look like: +``pkg.opam`` file to the root (``pkg.opam`` can be empty or generated +by Dune itself), and then providing ``dune`` files in the directories +your ``.v`` files are placed. For the experimental version "0.1" of +the Coq Dune language, |Coq| library stanzas look like: .. code:: scheme - (coqlib + (coq.theory (name <module_prefix>) - (public_name <package.lib_name>) + (package <opam_package>) (synopsis <text>) (modules <ordered_set_lang>) (libraries <ocaml_libraries>) (flags <coq_flags>)) This stanza will build all `.v` files in the given directory, wrapping -the library under ``<module_prefix>``. If you declare a -``<package.lib_name>`` a ``.install`` file for the library will be -generated; the optional ``<modules>`` field allows you to filter -the list of modules, and ``<libraries>`` allows to depend on ML -plugins. For the moment, Dune relies on Coq's standard mechanisms -(such as ``COQPATH``) to locate installed Coq libraries. +the library under ``<module_prefix>``. If you declare an +``<opam_package>``, an ``.install`` file for the library will be +generated; the optional ``(modules <ordered_set_lang>)`` field allows +you to filter the list of modules, and ``(libraries +<ocaml_libraries>)`` allows the Coq theory depend on ML plugins. For +the moment, Dune relies on Coq's standard mechanisms (such as +``COQPATH``) to locate installed Coq libraries. By default Dune will skip ``.v`` files present in subdirectories. In order to enable the usual recursive organization of Coq projects add @@ -565,9 +572,9 @@ of your project. .. code:: scheme - (coqlib + (coq.theory (name Equations) ; -R flag - (public_name equations.Equations) + (package equations) (synopsis "Equations Plugin") (libraries coq.plugins.extraction equations.plugin) (modules :standard \ IdDec NoCycle)) ; exclude some modules that don't build diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6a0ce20c79..d498c1ee2c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -72,7 +72,7 @@ specified, the default selector is used. .. _bindingslist: Bindings list -~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~ Tactics that take a term as an argument may also support a bindings list to instantiate some parameters of the term by name or position. @@ -1452,6 +1452,19 @@ Controlling the proof flow While :tacn:`pose proof` expects that no existential variables are generated by the tactic, :tacn:`epose proof` removes this constraint. +.. tacv:: pose proof (@ident := @term) + + This is an alternative syntax for :n:`assert (@ident := @term)` and + :n:`pose proof @term as @ident`, following the model of :n:`pose + (@ident := @term)` but dropping the value of :token:`ident`. + +.. tacv:: epose proof (@ident := @term) + + This is an alternative syntax for :n:`eassert (@ident := @term)` + and :n:`epose proof @term as @ident`, following the model of + :n:`epose (@ident := @term)` but dropping the value of + :token:`ident`. + .. tacv:: enough (@ident : @type) :name: enough @@ -3746,6 +3759,24 @@ automatically created. .. cmd:: Hint @hint_definition : {+ @ident} The general command to add a hint to some databases :n:`{+ @ident}`. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` + locality attributes. When no locality is explictly given, the + command is :attr:`local` inside a section and :attr:`global` otherwise. + + + :attr:`local` hints are never visible from other modules, even if they + require or import the current module. Inside a section, the :attr:`local` + attribute is useless since hints do not survive anyway to the closure of + sections. + + + :attr:`export` are visible from other modules when they import the current + module. Requiring it is not enough. This attribute is only effective for + the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and + :cmd:`Hint Extern` variants of the command. + + + :attr:`global` hints are made available by merely requiring the current + module. + The various possible :production:`hint_definition`\s are given below. .. cmdv:: Hint @hint_definition @@ -3754,25 +3785,18 @@ automatically created. .. deprecated:: 8.10 - .. cmdv:: Local Hint @hint_definition : {+ @ident} - - This is used to declare hints that must not be exported to the other modules - that require and import the current module. Inside a section, the flag - Local is useless since hints do not survive anyway to the closure of - sections. - - .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident + .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve - This command adds :n:`simple apply @term` to the hint list with the head - symbol of the type of :n:`@term`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The + This command adds :n:`simple apply @qualid` to the hint list with the head + symbol of the type of :n:`@qualid`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @qualid` or :n:`@num` if specified. The associated :n:`@pattern` is inferred from the conclusion of the type of - :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type - of :n:`@term` does not start with a product the tactic added in the hint list - is :n:`exact @term`. In case this type can however be reduced to a type - starting with a product, the tactic :n:`simple apply @term` is also stored in - the hints list. If the inferred type of :n:`@term` contains a dependent + :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@qualid` does not start with a product the tactic added in the hint list + is :n:`exact @qualid`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @qualid` is also stored in + the hints list. If the inferred type of :n:`@qualid` contains a dependent quantification on a variable which occurs only in the premisses of the type and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is added to the hint list @@ -3780,32 +3804,32 @@ automatically created. typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint - The head symbol of the type of :n:`@term` is a bound variable + The head symbol of the type of :n:`@qualid` is a bound variable such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Resolve {+ @term} : @ident + .. cmdv:: Hint Resolve {+ @qualid} : @ident - Adds each :n:`Hint Resolve @term`. + Adds each :n:`Hint Resolve @qualid`. - .. cmdv:: Hint Resolve -> @term : @ident + .. cmdv:: Hint Resolve -> @qualid : @ident Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentioned + the hint will be used as :n:`apply <- @qualid`, although as mentioned before, the tactic actually used is a restricted version of :tacn:`apply`). - .. cmdv:: Hint Resolve <- @term + .. cmdv:: Hint Resolve <- @qualid Adds the right-to-left implication of an equivalence as a hint. - .. cmdv:: Hint Immediate @term : @ident + .. cmdv:: Hint Immediate @qualid : @ident :name: Hint Immediate - This command adds :n:`simple apply @term; trivial` to the hint list associated + This command adds :n:`simple apply @qualid; trivial` to the hint list associated with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @term` are + tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are not solved immediately by the :tacn:`trivial` tactic (which only tries tactics with cost 0).This command is useful for theorems such as the symmetry of equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited @@ -3813,12 +3837,12 @@ automatically created. never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` itself. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint :undocumented: - .. cmdv:: Hint Immediate {+ @term} : @ident + .. cmdv:: Hint Immediate {+ @qualid} : @ident - Adds each :n:`Hint Immediate @term`. + Adds each :n:`Hint Immediate @qualid`. .. cmdv:: Hint Constructors @qualid : @ident :name: Hint Constructors @@ -4262,7 +4286,7 @@ some incompatibilities. :name: Firstorder Solver The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with *`, it can be reset locally or globally using this option. + :g:`auto with core`, it can be reset locally or globally using this option. .. cmd:: Print Firstorder Solver diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a38c26c2b3..4401f8fa2f 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -745,11 +745,6 @@ the toplevel, and using them in source files is discouraged. :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. - .. cmdv:: Add LoadPath @string - - Performs as :n:`Add LoadPath @string @dirpath` but - for the empty directory path. - .. cmd:: Add Rec LoadPath @string as @dirpath @@ -757,11 +752,6 @@ the toplevel, and using them in source files is discouraged. :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. - .. cmdv:: Add Rec LoadPath @string - - Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty - logical directory path. - .. cmd:: Remove LoadPath @string @@ -784,12 +774,6 @@ the toplevel, and using them in source files is discouraged. loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`). -.. cmd:: Add Rec ML Path @string - - This command adds the directory :n:`@string` and all its subdirectories to - the current OCaml loadpath (see the command :cmd:`Declare ML Module`). - - .. cmd:: Print ML Path @string This command displays the current OCaml loadpath. This @@ -1206,6 +1190,12 @@ Controlling the locality of commands 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. + .. _controlling-typing-flags: Controlling Typing Flags diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9b4d7cf5fa..669975ba7e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -909,10 +909,10 @@ notations are given below. The optional :production:`scope` is described in notation : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`]. : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`]. : [Local] Reserved Notation `string` [(`modifiers`)] . - : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. - : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. + : Inductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : CoInductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : Fixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. + : CoFixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. : [Local] Declare Custom Entry `ident`. modifiers : `modifier`, … , `modifier` modifier : at level `num` @@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in .. prodn:: decl_notations ::= where @decl_notation {* and @decl_notation } - decl_notation ::= @string := @term1_extended {? : @ident } + decl_notation ::= @string := @one_term {? ( only parsing ) } {? : @ident } .. note:: No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. @@ -1194,7 +1194,7 @@ Binding arguments of a constant to an interpretation scope Binding types of arguments to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++ -.. cmd:: Bind Scope @scope with @qualid +.. cmd:: Bind Scope @ident with {+ @class } When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 51688e2d9e..0f05237036 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -595,6 +595,7 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/SeqSeries.v theories/Reals/Sqrt_reg.v theories/Reals/Rlogic.v + theories/Reals/Rregisternames.v (theories/Reals/Reals.v) theories/Reals/Runcountable.v </dd> diff --git a/doc/tools/coqrst/__init__.py b/doc/tools/coqrst/__init__.py index 710a90a6f1..5720cd9be0 100644 --- a/doc/tools/coqrst/__init__.py +++ b/doc/tools/coqrst/__init__.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py index feafcba026..899c80fbe6 100644 --- a/doc/tools/coqrst/checkdeps.py +++ b/doc/tools/coqrst/checkdeps.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/coqdoc/__init__.py b/doc/tools/coqrst/coqdoc/__init__.py index 8d19924df1..3fe6886897 100644 --- a/doc/tools/coqrst/coqdoc/__init__.py +++ b/doc/tools/coqrst/coqdoc/__init__.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index adacba97cc..a3fc069e6c 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index d6ecf311f1..b92c94fe2c 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## @@ -294,7 +294,7 @@ class VernacObject(NotationObject): Example:: - .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident } + .. cmd:: Infix @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @ident } This command is equivalent to :n:`…`. """ diff --git a/doc/tools/coqrst/notations/Makefile b/doc/tools/coqrst/notations/Makefile index 29132f1cd7..dc3a647f9e 100644 --- a/doc/tools/coqrst/notations/Makefile +++ b/doc/tools/coqrst/notations/Makefile @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index f9cf26a21e..f29c69eeaf 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/tools/coqrst/notations/fontsupport.py b/doc/tools/coqrst/notations/fontsupport.py index c3ba2c1301..1ffd816ba7 100755 --- a/doc/tools/coqrst/notations/fontsupport.py +++ b/doc/tools/coqrst/notations/fontsupport.py @@ -2,8 +2,8 @@ # -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index 1136ee4997..7219fc2e37 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py index 7b7febe668..abefd97121 100644 --- a/doc/tools/coqrst/notations/parsing.py +++ b/doc/tools/coqrst/notations/parsing.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py index 23996b0d63..2a8bf76e75 100644 --- a/doc/tools/coqrst/notations/plain.py +++ b/doc/tools/coqrst/notations/plain.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/regexp.py b/doc/tools/coqrst/notations/regexp.py index 697201a5d5..5979fe8f82 100644 --- a/doc/tools/coqrst/notations/regexp.py +++ b/doc/tools/coqrst/notations/regexp.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index 5659a64b84..158a703640 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py index 6d9c79d16c..9e23be2409 100644 --- a/doc/tools/coqrst/repl/ansicolors.py +++ b/doc/tools/coqrst/repl/ansicolors.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 3dc20db82b..c306961550 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index fc6d0ace0d..8f325f957a 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -1,12 +1,13 @@ # Grammar extraction tool for documentation -`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it in -chunks into `.rst` files. The tool currently inserts Sphinx -`productionlist` constructs. It also generates a file with `prodn` constructs -for the entire grammar, but updates to `tacn` and `cmd` constructs must be done -manually since the grammar doesn't have names for them as it does for -nonterminals. There is an option to report which `tacn` and `cmd` were not -found in the `.rst` files. `tacv` and `cmdv` constructs are not processed at all. +`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and +inserts it in chunks into `.rst` files. The tool currently inserts +Sphinx `productionlist` and `prodn` constructs (`productionlist` are +gradually being replaced by `prodn` in the manual). Updates to `tacn` +and `cmd` constructs must be done manually since the grammar doesn't +have names for them as it does for nonterminals. There is an option +to report which `tacn` and `cmd` were not found in the `.rst` files. +`tacv` and `cmdv` constructs are not processed at all. The mlg grammars present several challenges to generating an accurate grammar for documentation purposes: diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 3524d77380..fe2e68a517 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -57,14 +57,15 @@ DELETE: [ | check_for_coloneq | local_test_lpar_id_colon | lookup_at_as_comma -| only_starredidentrefs +| test_only_starredidentrefs | test_bracket_ident | test_lpar_id_colon | test_lpar_id_coloneq (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *) | test_lpar_id_rpar | test_lpar_idnum_coloneq -| test_nospace_pipe_closedcurly | test_show_goal +| test_name_colon +| test_pipe_closedcurly | ensure_fixannot (* SSR *) @@ -332,8 +333,8 @@ typeclass_constraint: [ | EDIT ADD_OPT "!" operconstr200 | REPLACE "{" name "}" ":" [ "!" | ] operconstr200 | WITH "{" name "}" ":" OPT "!" operconstr200 -| REPLACE name_colon [ "!" | ] operconstr200 -| WITH name_colon OPT "!" operconstr200 +| REPLACE name ":" [ "!" | ] operconstr200 +| WITH name ":" OPT "!" operconstr200 ] (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*) @@ -409,19 +410,6 @@ DELETE: [ | cumulativity_token ] -opt_coercion: [ -| OPTINREF -] - -opt_constructors_or_fields: [ -| OPTINREF -] - -SPLICE: [ -| opt_coercion -| opt_constructors_or_fields -] - constructor_list_or_record_decl: [ | OPTINREF ] @@ -433,11 +421,6 @@ record_fields: [ | DELETE (* empty *) ] -decl_notation: [ -| REPLACE "where" LIST1 one_decl_notation SEP decl_sep -| WITH "where" one_decl_notation LIST0 ( decl_sep one_decl_notation ) -] - assumptions_token: [ | DELETENT ] @@ -767,13 +750,13 @@ vernacular: [ ] rec_definition: [ -| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation -| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations +| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] corec_definition: [ -| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation -| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations +| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] type_cstr: [ @@ -782,13 +765,9 @@ type_cstr: [ | OPTINREF ] -decl_notation: [ -| OPTINREF -] - inductive_definition: [ -| REPLACE OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation -| WITH OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation +| REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations +| WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations ] constructor_list_or_record_decl: [ @@ -807,6 +786,31 @@ record_binder: [ | DELETE name ] +in_clause: [ +| DELETE in_clause' +| REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ +| WITH LIST0 hypident_occ SEP "," OPT ( "|-" concl_occ ) +| DELETE LIST0 hypident_occ SEP "," +] + +concl_occ: [ +| OPTINREF +] + +opt_coercion: [ +| OPTINREF +] + +opt_constructors_or_fields: [ +| OPTINREF +] + +decl_notations: [ +| REPLACE "where" LIST1 decl_notation SEP decl_sep +| WITH "where" decl_notation LIST0 (decl_sep decl_notation ) +| OPTINREF +] + SPLICE: [ | noedit_mode | command_entry @@ -941,11 +945,12 @@ SPLICE: [ | record_fields | constructor_type | record_binder +| opt_coercion +| opt_constructors_or_fields ] (* end SPLICE *) RENAME: [ | clause clause_dft_concl -| in_clause' in_clause | tactic3 ltac_expr3 (* todo: can't figure out how this gets mapped by coqpp *) | tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *) @@ -980,7 +985,7 @@ RENAME: [ | nat_or_var num_or_var | fix_decl fix_body | cofix_decl cofix_body -| constr term1_extended +| constr one_term | appl_arg arg | rec_definition fix_definition | corec_definition cofix_definition @@ -988,12 +993,12 @@ RENAME: [ | univ_instance univ_annot | simple_assum_coe assumpt | of_type_with_opt_coercion of_type -| decl_notation decl_notations -| one_decl_notation decl_notation | attribute attr | attribute_value attr_value | constructor_list_or_record_decl constructors_or_record | record_binder_body field_body +| class_rawexpr class +| smart_global smart_qualid ] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 5fcb56f5f2..5c9a13668f 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -1717,7 +1717,7 @@ let process_rst g file args seen tac_prods cmd_prods = else begin let line3 = getline() in if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "prodn::" then - error "%s line %d: expecting 'prodn' after 'insertprodn'\n" file !linenum + error "%s line %d: expecting '.. prodn::' after 'insertprodn'\n" file !linenum else begin let indent = Str.matched_group 1 line3 in let rec skip_to_end () = diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune new file mode 100644 index 0000000000..3afa21f2cf --- /dev/null +++ b/doc/tools/docgram/dune @@ -0,0 +1,30 @@ +(executable + (name doc_grammar) + (libraries coq.clib coqpp)) + +(env (_ (binaries doc_grammar.exe))) + +(rule + (targets fullGrammar) + (deps + ; Main grammar + (glob_files %{project_root}/parsing/*.mlg) + (glob_files %{project_root}/toplevel/*.mlg) + (glob_files %{project_root}/vernac/*.mlg) + ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) + (glob_files %{project_root}/plugins/btauto/*.mlg) + (glob_files %{project_root}/plugins/cc/*.mlg) + (glob_files %{project_root}/plugins/derive/*.mlg) + (glob_files %{project_root}/plugins/extraction/*.mlg) + (glob_files %{project_root}/plugins/firstorder/*.mlg) + (glob_files %{project_root}/plugins/funind/*.mlg) + (glob_files %{project_root}/plugins/ltac/*.mlg) + (glob_files %{project_root}/plugins/micromega/*.mlg) + (glob_files %{project_root}/plugins/nsatz/*.mlg) + (glob_files %{project_root}/plugins/omega/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/setoid_ring/*.mlg) + (glob_files %{project_root}/plugins/syntax/*.mlg)) + (action + (chdir %{project_root} (run doc_grammar -short -no-warn %{deps}))) + (mode promote)) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 529d81e424..6897437457 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -152,7 +152,7 @@ binder_constr: [ ] appl_arg: [ -| lpar_id_coloneq lconstr ")" +| test_lpar_id_coloneq "(" ident ":=" lconstr ")" | operconstr9 ] @@ -335,7 +335,7 @@ closed_binder: [ typeclass_constraint: [ | "!" operconstr200 | "{" name "}" ":" [ "!" | ] operconstr200 -| name_colon [ "!" | ] operconstr200 +| test_name_colon name ":" [ "!" | ] operconstr200 | operconstr200 ] @@ -449,7 +449,7 @@ bigint: [ ] bar_cbrace: [ -| test_nospace_pipe_closedcurly "|" "}" +| test_pipe_closedcurly "|" "}" ] vernac_toplevel: [ @@ -511,8 +511,8 @@ command: [ | "Load" [ "Verbose" | ] [ ne_string | IDENT ] | "Declare" "ML" "Module" LIST1 ne_string | "Locate" locatable -| "Add" "LoadPath" ne_string as_dirpath -| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Add" "LoadPath" ne_string "as" dirpath +| "Add" "Rec" "LoadPath" ne_string "as" dirpath | "Remove" "LoadPath" ne_string | "Type" lconstr | "Print" printable @@ -522,7 +522,6 @@ command: [ | "Print" "Namespace" dirpath | "Inspect" natural | "Add" "ML" "Path" ne_string -| "Add" "Rec" "ML" "Path" ne_string | "Set" option_table option_setting | "Unset" option_table | "Print" "Table" option_table @@ -655,6 +654,7 @@ command: [ | "Add" "CstOp" constr (* micromega plugin *) | "Add" "BinRel" constr (* micromega plugin *) | "Add" "PropOp" constr (* micromega plugin *) +| "Add" "PropBinOp" constr (* micromega plugin *) | "Add" "PropUOp" constr (* micromega plugin *) | "Add" "Spec" constr (* micromega plugin *) | "Add" "BinOpSpec" constr (* micromega plugin *) @@ -924,16 +924,16 @@ reduce: [ | ] -one_decl_notation: [ -| ne_lstring ":=" constr OPT [ ":" IDENT ] +decl_notation: [ +| ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ] ] decl_sep: [ | "and" ] -decl_notation: [ -| "where" LIST1 one_decl_notation SEP decl_sep +decl_notations: [ +| "where" LIST1 decl_notation SEP decl_sep | ] @@ -943,7 +943,7 @@ opt_constructors_or_fields: [ ] inductive_definition: [ -| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation +| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations ] constructor_list_or_record_decl: [ @@ -961,11 +961,11 @@ opt_coercion: [ ] rec_definition: [ -| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] corec_definition: [ -| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] scheme: [ @@ -982,7 +982,7 @@ scheme_kind: [ ] record_field: [ -| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation +| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notations ] record_fields: [ @@ -1148,7 +1148,7 @@ module_type: [ ] section_subset_expr: [ -| only_starredidentrefs LIST0 starredidentref +| test_only_starredidentrefs LIST0 starredidentref | ssexpr35 ] @@ -1172,8 +1172,8 @@ ssexpr50: [ ssexpr0: [ | starredidentref -| "(" only_starredidentrefs LIST0 starredidentref ")" -| "(" only_starredidentrefs LIST0 starredidentref ")" "*" +| "(" test_only_starredidentrefs LIST0 starredidentref ")" +| "(" test_only_starredidentrefs LIST0 starredidentref ")" "*" | "(" ssexpr35 ")" | "(" ssexpr35 ")" "*" ] @@ -1331,10 +1331,6 @@ option_table: [ | LIST1 IDENT ] -as_dirpath: [ -| OPT [ "as" dirpath ] -] - ne_in_or_out_modules: [ | "inside" LIST1 global | "outside" LIST1 global @@ -1684,6 +1680,8 @@ simple_tactic: [ | "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic | "assert" constr as_ipat by_tactic | "eassert" constr as_ipat by_tactic +| "pose" "proof" test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| "epose" "proof" test_lpar_id_coloneq "(" identref ":=" lconstr ")" | "pose" "proof" lconstr as_ipat | "epose" "proof" lconstr as_ipat | "enough" constr as_ipat by_tactic @@ -1740,10 +1738,11 @@ simple_tactic: [ | "psatz_R" tactic (* micromega plugin *) | "psatz_Q" int_or_var tactic (* micromega plugin *) | "psatz_Q" tactic (* micromega plugin *) -| "zify_iter_specs" tactic (* micromega plugin *) +| "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) | "zify_saturate" (* micromega plugin *) | "zify_iter_let" tactic (* micromega plugin *) +| "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) | "omega" (* omega plugin *) | "rtauto" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 908e3ccd51..f26a174722 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -58,6 +58,11 @@ arg: [ | term1 ] +one_term: [ +| term1 +| "@" qualid OPT univ_annot +] + term1: [ | term_projection | term0 "%" ident @@ -238,13 +243,8 @@ fix_body: [ fixannot: [ | "{" "struct" ident "}" -| "{" "wf" term1_extended ident "}" -| "{" "measure" term1_extended OPT ident OPT term1_extended "}" -] - -term1_extended: [ -| term1 -| "@" qualid OPT univ_annot +| "{" "wf" one_term ident "}" +| "{" "measure" one_term OPT ident OPT one_term "}" ] term_cofix: [ @@ -400,7 +400,7 @@ decl_notations: [ ] decl_notation: [ -| string ":=" term1_extended OPT [ ":" ident ] +| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ] ] register_token: [ @@ -484,16 +484,16 @@ red_expr: [ | "vm_compute" OPT ref_or_pattern_occ | "native_compute" OPT ref_or_pattern_occ | "unfold" LIST1 unfold_occ SEP "," -| "fold" LIST1 term1_extended +| "fold" LIST1 one_term | "pattern" LIST1 pattern_occ SEP "," | ident ] delta_flag: [ -| OPT "-" "[" LIST1 smart_global "]" +| OPT "-" "[" LIST1 smart_qualid "]" ] -smart_global: [ +smart_qualid: [ | qualid | by_notation ] @@ -518,8 +518,8 @@ red_flags: [ ] ref_or_pattern_occ: [ -| smart_global OPT ( "at" occs_nums ) -| term1_extended OPT ( "at" occs_nums ) +| smart_qualid OPT ( "at" occs_nums ) +| one_term OPT ( "at" occs_nums ) ] occs_nums: [ @@ -538,11 +538,11 @@ int_or_var: [ ] unfold_occ: [ -| smart_global OPT ( "at" occs_nums ) +| smart_qualid OPT ( "at" occs_nums ) ] pattern_occ: [ -| term1_extended OPT ( "at" occs_nums ) +| one_term OPT ( "at" occs_nums ) ] finite_token: [ @@ -587,11 +587,11 @@ scheme: [ ] scheme_kind: [ -| "Induction" "for" smart_global "Sort" sort_family -| "Minimality" "for" smart_global "Sort" sort_family -| "Elimination" "for" smart_global "Sort" sort_family -| "Case" "for" smart_global "Sort" sort_family -| "Equality" "for" smart_global +| "Induction" "for" smart_qualid "Sort" sort_family +| "Minimality" "for" smart_qualid "Sort" sort_family +| "Elimination" "for" smart_qualid "Sort" sort_family +| "Case" "for" smart_qualid "Sort" sort_family +| "Equality" "for" smart_qualid ] sort_family: [ @@ -615,21 +615,21 @@ gallina_ext: [ | "Export" LIST1 qualid | "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) | "Include" "Type" module_type_inl LIST0 ( "<+" module_type_inl ) -| "Transparent" LIST1 smart_global -| "Opaque" LIST1 smart_global -| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ] +| "Transparent" LIST1 smart_qualid +| "Opaque" LIST1 smart_qualid +| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ] | "Canonical" OPT "Structure" qualid OPT [ OPT univ_decl def_body ] | "Canonical" OPT "Structure" by_notation | "Coercion" qualid OPT univ_decl def_body -| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr -| "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr -| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Identity" "Coercion" ident ":" class ">->" class +| "Coercion" qualid ":" class ">->" class +| "Coercion" by_notation ":" class ">->" class | "Context" LIST1 binder | "Instance" instance_name ":" term hint_info [ ":=" "{" [ LIST1 field_def SEP ";" | ] "}" | ":=" term | ] | "Existing" "Instance" qualid hint_info | "Existing" "Instances" LIST1 qualid OPT [ "|" num ] | "Existing" "Class" qualid -| "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] | "Implicit" "Type" reserv_list | "Implicit" "Types" reserv_list | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ] @@ -643,14 +643,8 @@ option_setting: [ | string ] -class_rawexpr: [ -| "Funclass" -| "Sortclass" -| smart_global -] - hint_info: [ -| "|" OPT num OPT term1_extended +| "|" OPT num OPT one_term | ] @@ -780,11 +774,11 @@ command: [ | "Load" [ "Verbose" | ] [ string | ident ] | "Declare" "ML" "Module" LIST1 string | "Locate" locatable -| "Add" "LoadPath" string as_dirpath -| "Add" "Rec" "LoadPath" string as_dirpath +| "Add" "LoadPath" string "as" dirpath +| "Add" "Rec" "LoadPath" string "as" dirpath | "Remove" "LoadPath" string | "Type" term -| "Print" "Term" smart_global OPT ( "@{" LIST0 name "}" ) +| "Print" "Term" smart_qualid OPT ( "@{" LIST0 name "}" ) | "Print" "All" | "Print" "Section" qualid | "Print" "Grammar" ident @@ -798,36 +792,35 @@ command: [ | "Print" "Graph" | "Print" "Classes" | "Print" "TypeClasses" -| "Print" "Instances" smart_global +| "Print" "Instances" smart_qualid | "Print" "Coercions" -| "Print" "Coercion" "Paths" class_rawexpr class_rawexpr -| "Print" "Canonical" "Projections" LIST0 smart_global +| "Print" "Coercion" "Paths" class class +| "Print" "Canonical" "Projections" LIST0 smart_qualid | "Print" "Typing" "Flags" | "Print" "Tables" | "Print" "Options" | "Print" "Hint" -| "Print" "Hint" smart_global +| "Print" "Hint" smart_qualid | "Print" "Hint" "*" | "Print" "HintDb" ident | "Print" "Scopes" | "Print" "Scope" ident | "Print" "Visibility" OPT ident -| "Print" "Implicit" smart_global +| "Print" "Implicit" smart_qualid | "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string -| "Print" "Assumptions" smart_global -| "Print" "Opaque" "Dependencies" smart_global -| "Print" "Transparent" "Dependencies" smart_global -| "Print" "All" "Dependencies" smart_global -| "Print" "Strategy" smart_global +| "Print" "Assumptions" smart_qualid +| "Print" "Opaque" "Dependencies" smart_qualid +| "Print" "Transparent" "Dependencies" smart_qualid +| "Print" "All" "Dependencies" smart_qualid +| "Print" "Strategy" smart_qualid | "Print" "Strategies" | "Print" "Registered" -| "Print" smart_global OPT ( "@{" LIST0 name "}" ) +| "Print" smart_qualid OPT ( "@{" LIST0 name "}" ) | "Print" "Module" "Type" qualid | "Print" "Module" qualid | "Print" "Namespace" dirpath | "Inspect" num | "Add" "ML" "Path" string -| "Add" "Rec" "ML" "Path" string | "Set" LIST1 ident option_setting | "Unset" LIST1 ident | "Print" "Table" LIST1 ident @@ -849,7 +842,7 @@ command: [ | "Debug" "Off" | "Declare" "Reduction" ident ":=" red_expr | "Declare" "Custom" "Entry" ident -| "Derive" ident "SuchThat" term1_extended "As" ident (* derive plugin *) +| "Derive" ident "SuchThat" one_term "As" ident (* derive plugin *) | "Proof" | "Proof" "Mode" string | "Proof" term @@ -907,31 +900,31 @@ command: [ | "Obligations" | "Preterm" "of" ident | "Preterm" -| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Setoid" term1_extended term1_extended term1_extended "as" ident -| "Add" "Parametric" "Setoid" LIST0 binder ":" term1_extended term1_extended term1_extended "as" ident -| "Add" "Morphism" term1_extended ":" ident -| "Declare" "Morphism" term1_extended ":" ident -| "Add" "Morphism" term1_extended "with" "signature" term "as" ident -| "Add" "Parametric" "Morphism" LIST0 binder ":" term1_extended "with" "signature" term "as" ident +| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "as" ident +| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Setoid" one_term one_term one_term "as" ident +| "Add" "Parametric" "Setoid" LIST0 binder ":" one_term one_term one_term "as" ident +| "Add" "Morphism" one_term ":" ident +| "Declare" "Morphism" one_term ":" ident +| "Add" "Morphism" one_term "with" "signature" term "as" ident +| "Add" "Parametric" "Morphism" LIST0 binder ":" one_term "with" "signature" term "as" ident | "Grab" "Existential" "Variables" | "Unshelve" -| "Declare" "Equivalent" "Keys" term1_extended term1_extended +| "Declare" "Equivalent" "Keys" one_term one_term | "Print" "Equivalent" "Keys" | "Optimize" "Proof" | "Optimize" "Heap" @@ -940,24 +933,25 @@ command: [ | "Show" "Ltac" "Profile" "CutOff" int | "Show" "Ltac" "Profile" string | "Show" "Lia" "Profile" (* micromega plugin *) -| "Add" "InjTyp" term1_extended (* micromega plugin *) -| "Add" "BinOp" term1_extended (* micromega plugin *) -| "Add" "UnOp" term1_extended (* micromega plugin *) -| "Add" "CstOp" term1_extended (* micromega plugin *) -| "Add" "BinRel" term1_extended (* micromega plugin *) -| "Add" "PropOp" term1_extended (* micromega plugin *) -| "Add" "PropUOp" term1_extended (* micromega plugin *) -| "Add" "Spec" term1_extended (* micromega plugin *) -| "Add" "BinOpSpec" term1_extended (* micromega plugin *) -| "Add" "UnOpSpec" term1_extended (* micromega plugin *) -| "Add" "Saturate" term1_extended (* micromega plugin *) +| "Add" "InjTyp" one_term (* micromega plugin *) +| "Add" "BinOp" one_term (* micromega plugin *) +| "Add" "UnOp" one_term (* micromega plugin *) +| "Add" "CstOp" one_term (* micromega plugin *) +| "Add" "BinRel" one_term (* micromega plugin *) +| "Add" "PropOp" one_term (* micromega plugin *) +| "Add" "PropBinOp" one_term (* micromega plugin *) +| "Add" "PropUOp" one_term (* micromega plugin *) +| "Add" "Spec" one_term (* micromega plugin *) +| "Add" "BinOpSpec" one_term (* micromega plugin *) +| "Add" "UnOpSpec" one_term (* micromega plugin *) +| "Add" "Saturate" one_term (* micromega plugin *) | "Show" "Zify" "InjTyp" (* micromega plugin *) | "Show" "Zify" "BinOp" (* micromega plugin *) | "Show" "Zify" "UnOp" (* micromega plugin *) | "Show" "Zify" "CstOp" (* micromega plugin *) | "Show" "Zify" "BinRel" (* micromega plugin *) | "Show" "Zify" "Spec" (* micromega plugin *) -| "Add" "Ring" ident ":" term1_extended OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* setoid_ring plugin *) +| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* setoid_ring plugin *) | "Hint" "Cut" "[" hints_path "]" opthints | "Typeclasses" "Transparent" LIST0 qualid | "Typeclasses" "Opaque" LIST0 qualid @@ -996,20 +990,20 @@ command: [ | "Show" "Extraction" (* extraction plugin *) | "Functional" "Case" fun_scheme_arg (* funind plugin *) | "Generate" "graph" "for" qualid (* funind plugin *) -| "Hint" "Rewrite" orient LIST1 term1_extended ":" LIST0 ident -| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr ":" LIST0 ident -| "Hint" "Rewrite" orient LIST1 term1_extended -| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr -| "Derive" "Inversion_clear" ident "with" term1_extended "Sort" sort_family -| "Derive" "Inversion_clear" ident "with" term1_extended -| "Derive" "Inversion" ident "with" term1_extended "Sort" sort_family -| "Derive" "Inversion" ident "with" term1_extended -| "Derive" "Dependent" "Inversion" ident "with" term1_extended "Sort" sort_family -| "Derive" "Dependent" "Inversion_clear" ident "with" term1_extended "Sort" sort_family -| "Declare" "Left" "Step" term1_extended -| "Declare" "Right" "Step" term1_extended +| "Hint" "Rewrite" orient LIST1 one_term ":" LIST0 ident +| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr ":" LIST0 ident +| "Hint" "Rewrite" orient LIST1 one_term +| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr +| "Derive" "Inversion_clear" ident "with" one_term "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" one_term +| "Derive" "Inversion" ident "with" one_term "Sort" sort_family +| "Derive" "Inversion" ident "with" one_term +| "Derive" "Dependent" "Inversion" ident "with" one_term "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family +| "Declare" "Left" "Step" one_term +| "Declare" "Right" "Step" one_term | "Print" "Rings" (* setoid_ring plugin *) -| "Add" "Field" ident ":" term1_extended OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) +| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) | "Print" "Fields" (* setoid_ring plugin *) | "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption | "String" "Notation" qualid qualid qualid ":" ident @@ -1059,8 +1053,8 @@ dirpath: [ ] locatable: [ -| smart_global -| "Term" smart_global +| smart_qualid +| "Term" smart_qualid | "File" string | "Library" qualid | "Module" qualid @@ -1071,19 +1065,15 @@ option_ref_value: [ | string ] -as_dirpath: [ -| OPT [ "as" dirpath ] -] - comment: [ -| term1_extended +| one_term | string | num ] reference_or_constr: [ | qualid -| term1_extended +| one_term ] hint: [ @@ -1100,7 +1090,7 @@ hint: [ | "Mode" qualid LIST1 [ "+" | "!" | "-" ] | "Unfold" LIST1 qualid | "Constructors" LIST1 qualid -| "Extern" num OPT term1_extended "=>" ltac_expr +| "Extern" num OPT one_term "=>" ltac_expr ] constr_body: [ @@ -1157,23 +1147,23 @@ fun_scheme_arg: [ ] ring_mod: [ -| "decidable" term1_extended (* setoid_ring plugin *) +| "decidable" one_term (* setoid_ring plugin *) | "abstract" (* setoid_ring plugin *) -| "morphism" term1_extended (* setoid_ring plugin *) +| "morphism" one_term (* setoid_ring plugin *) | "constants" "[" ltac_expr "]" (* setoid_ring plugin *) -| "closed" "[" LIST1 qualid "]" (* setoid_ring plugin *) | "preprocess" "[" ltac_expr "]" (* setoid_ring plugin *) | "postprocess" "[" ltac_expr "]" (* setoid_ring plugin *) -| "setoid" term1_extended term1_extended (* setoid_ring plugin *) -| "sign" term1_extended (* setoid_ring plugin *) -| "power" term1_extended "[" LIST1 qualid "]" (* setoid_ring plugin *) -| "power_tac" term1_extended "[" ltac_expr "]" (* setoid_ring plugin *) -| "div" term1_extended (* setoid_ring plugin *) +| "setoid" one_term one_term (* setoid_ring plugin *) +| "sign" one_term (* setoid_ring plugin *) +| "power" one_term "[" LIST1 qualid "]" (* setoid_ring plugin *) +| "power_tac" one_term "[" ltac_expr "]" (* setoid_ring plugin *) +| "div" one_term (* setoid_ring plugin *) +| "closed" "[" LIST1 qualid "]" (* setoid_ring plugin *) ] field_mod: [ | ring_mod (* setoid_ring plugin *) -| "completeness" term1_extended (* setoid_ring plugin *) +| "completeness" one_term (* setoid_ring plugin *) ] debug: [ @@ -1216,15 +1206,21 @@ query_command: [ | "Eval" red_expr "in" term "." | "Compute" term "." | "Check" term "." -| "About" smart_global OPT ( "@{" LIST0 name "}" ) "." -| "SearchHead" term1_extended in_or_out_modules "." -| "SearchPattern" term1_extended in_or_out_modules "." -| "SearchRewrite" term1_extended in_or_out_modules "." +| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) "." +| "SearchHead" one_term in_or_out_modules "." +| "SearchPattern" one_term in_or_out_modules "." +| "SearchRewrite" one_term in_or_out_modules "." | "Search" searchabout_query searchabout_queries "." | "SearchAbout" searchabout_query searchabout_queries "." | "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." ] +class: [ +| "Funclass" +| "Sortclass" +| smart_qualid +] + ne_in_or_out_modules: [ | "inside" LIST1 qualid | "outside" LIST1 qualid @@ -1242,7 +1238,7 @@ positive_search_mark: [ searchabout_query: [ | positive_search_mark string OPT ( "%" ident ) -| positive_search_mark term1_extended +| positive_search_mark one_term ] searchabout_queries: [ @@ -1256,10 +1252,10 @@ syntax: [ | "Close" "Scope" ident | "Delimit" "Scope" ident "with" ident | "Undelimit" "Scope" ident -| "Bind" "Scope" ident "with" LIST1 class_rawexpr -| "Infix" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] -| "Notation" ident LIST0 ident ":=" term1_extended OPT ( "(" "only" "parsing" ")" ) -| "Notation" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] +| "Bind" "Scope" ident "with" LIST1 class +| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] +| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) +| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] | "Format" "Notation" string string string | "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] | "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] @@ -1314,17 +1310,17 @@ at_level_opt: [ simple_tactic: [ | "reflexivity" -| "exact" term1_extended +| "exact" one_term | "assumption" | "etransitivity" -| "cut" term1_extended -| "exact_no_check" term1_extended -| "vm_cast_no_check" term1_extended -| "native_cast_no_check" term1_extended -| "casetype" term1_extended -| "elimtype" term1_extended -| "lapply" term1_extended -| "transitivity" term1_extended +| "cut" one_term +| "exact_no_check" one_term +| "vm_cast_no_check" one_term +| "native_cast_no_check" one_term +| "casetype" one_term +| "elimtype" one_term +| "lapply" one_term +| "transitivity" one_term | "left" | "eleft" | "left" "with" bindings @@ -1377,11 +1373,11 @@ simple_tactic: [ | "clear" LIST0 ident | "clear" "-" LIST1 ident | "clearbody" LIST1 ident -| "generalize" "dependent" term1_extended -| "replace" term1_extended "with" term1_extended clause_dft_concl by_arg_tac -| "replace" "->" term1_extended clause_dft_concl -| "replace" "<-" term1_extended clause_dft_concl -| "replace" term1_extended clause_dft_concl +| "generalize" "dependent" one_term +| "replace" one_term "with" one_term clause_dft_concl by_arg_tac +| "replace" "->" one_term clause_dft_concl +| "replace" "<-" one_term clause_dft_concl +| "replace" one_term clause_dft_concl | "simplify_eq" | "simplify_eq" destruction_arg | "esimplify_eq" @@ -1400,64 +1396,64 @@ simple_tactic: [ | "einjection" destruction_arg "as" LIST0 simple_intropattern | "simple" "injection" | "simple" "injection" destruction_arg -| "dependent" "rewrite" orient term1_extended -| "dependent" "rewrite" orient term1_extended "in" ident -| "cutrewrite" orient term1_extended -| "cutrewrite" orient term1_extended "in" ident -| "decompose" "sum" term1_extended -| "decompose" "record" term1_extended -| "absurd" term1_extended +| "dependent" "rewrite" orient one_term +| "dependent" "rewrite" orient one_term "in" ident +| "cutrewrite" orient one_term +| "cutrewrite" orient one_term "in" ident +| "decompose" "sum" one_term +| "decompose" "record" one_term +| "absurd" one_term | "contradiction" OPT constr_with_bindings | "autorewrite" "with" LIST1 ident clause_dft_concl | "autorewrite" "with" LIST1 ident clause_dft_concl "using" ltac_expr | "autorewrite" "*" "with" LIST1 ident clause_dft_concl | "autorewrite" "*" "with" LIST1 ident clause_dft_concl "using" ltac_expr -| "rewrite" "*" orient term1_extended "in" ident "at" occurrences by_arg_tac -| "rewrite" "*" orient term1_extended "at" occurrences "in" ident by_arg_tac -| "rewrite" "*" orient term1_extended "in" ident by_arg_tac -| "rewrite" "*" orient term1_extended "at" occurrences by_arg_tac -| "rewrite" "*" orient term1_extended by_arg_tac -| "refine" term1_extended -| "simple" "refine" term1_extended -| "notypeclasses" "refine" term1_extended -| "simple" "notypeclasses" "refine" term1_extended +| "rewrite" "*" orient one_term "in" ident "at" occurrences by_arg_tac +| "rewrite" "*" orient one_term "at" occurrences "in" ident by_arg_tac +| "rewrite" "*" orient one_term "in" ident by_arg_tac +| "rewrite" "*" orient one_term "at" occurrences by_arg_tac +| "rewrite" "*" orient one_term by_arg_tac +| "refine" one_term +| "simple" "refine" one_term +| "notypeclasses" "refine" one_term +| "simple" "notypeclasses" "refine" one_term | "solve_constraints" | "subst" LIST1 ident | "subst" | "simple" "subst" | "evar" "(" ident ":" term ")" -| "evar" term1_extended +| "evar" one_term | "instantiate" "(" ident ":=" term ")" | "instantiate" "(" int ":=" term ")" hloc | "instantiate" -| "stepl" term1_extended "by" ltac_expr -| "stepl" term1_extended -| "stepr" term1_extended "by" ltac_expr -| "stepr" term1_extended +| "stepl" one_term "by" ltac_expr +| "stepl" one_term +| "stepr" one_term "by" ltac_expr +| "stepr" one_term | "generalize_eqs" ident | "dependent" "generalize_eqs" ident | "generalize_eqs_vars" ident | "dependent" "generalize_eqs_vars" ident | "specialize_eqs" ident -| "hresolve_core" "(" ident ":=" term1_extended ")" "at" int_or_var "in" term1_extended -| "hresolve_core" "(" ident ":=" term1_extended ")" "in" term1_extended +| "hresolve_core" "(" ident ":=" one_term ")" "at" int_or_var "in" one_term +| "hresolve_core" "(" ident ":=" one_term ")" "in" one_term | "hget_evar" int_or_var | "destauto" | "destauto" "in" ident | "transparent_abstract" ltac_expr3 | "transparent_abstract" ltac_expr3 "using" ident -| "constr_eq" term1_extended term1_extended -| "constr_eq_strict" term1_extended term1_extended -| "constr_eq_nounivs" term1_extended term1_extended -| "is_evar" term1_extended -| "has_evar" term1_extended -| "is_var" term1_extended -| "is_fix" term1_extended -| "is_cofix" term1_extended -| "is_ind" term1_extended -| "is_constructor" term1_extended -| "is_proj" term1_extended -| "is_const" term1_extended +| "constr_eq" one_term one_term +| "constr_eq_strict" one_term one_term +| "constr_eq_nounivs" one_term one_term +| "is_evar" one_term +| "has_evar" one_term +| "is_var" one_term +| "is_fix" one_term +| "is_cofix" one_term +| "is_ind" one_term +| "is_constructor" one_term +| "is_proj" one_term +| "is_const" one_term | "shelve" | "shelve_unifiable" | "unshelve" ltac_expr1 @@ -1466,7 +1462,7 @@ simple_tactic: [ | "swap" int_or_var int_or_var | "revgoals" | "guard" int_or_var comparison int_or_var -| "decompose" "[" LIST1 term1_extended "]" term1_extended +| "decompose" "[" LIST1 one_term "]" one_term | "optimize_heap" | "start" "ltac" "profiling" | "stop" "ltac" "profiling" @@ -1478,14 +1474,14 @@ simple_tactic: [ | "finish_timing" OPT string | "finish_timing" "(" string ")" OPT string | "eassumption" -| "eexact" term1_extended +| "eexact" one_term | "trivial" auto_using hintbases | "info_trivial" auto_using hintbases | "debug" "trivial" auto_using hintbases | "auto" OPT int_or_var auto_using hintbases | "info_auto" OPT int_or_var auto_using hintbases | "debug" "auto" OPT int_or_var auto_using hintbases -| "prolog" "[" LIST0 term1_extended "]" int_or_var +| "prolog" "[" LIST0 one_term "]" int_or_var | "eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "new" "auto" OPT int_or_var auto_using hintbases | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases @@ -1494,17 +1490,17 @@ simple_tactic: [ | "autounfold" hintbases clause_dft_concl | "autounfold_one" hintbases "in" ident | "autounfold_one" hintbases -| "unify" term1_extended term1_extended -| "unify" term1_extended term1_extended "with" ident -| "convert_concl_no_check" term1_extended +| "unify" one_term one_term +| "unify" one_term one_term "with" ident +| "convert_concl_no_check" one_term | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 ident | "typeclasses" "eauto" OPT int_or_var "with" LIST1 ident | "typeclasses" "eauto" OPT int_or_var -| "head_of_constr" ident term1_extended -| "not_evar" term1_extended -| "is_ground" term1_extended -| "autoapply" term1_extended "using" ident -| "autoapply" term1_extended "with" ident +| "head_of_constr" ident one_term +| "not_evar" one_term +| "is_ground" one_term +| "autoapply" one_term "using" ident +| "autoapply" one_term "with" ident | "progress_evars" ltac_expr | "rewrite_strat" rewstrategy | "rewrite_db" ident "in" ident @@ -1518,10 +1514,10 @@ simple_tactic: [ | "setoid_symmetry" | "setoid_symmetry" "in" ident | "setoid_reflexivity" -| "setoid_transitivity" term1_extended +| "setoid_transitivity" one_term | "setoid_etransitivity" | "decide" "equality" -| "compare" term1_extended term1_extended +| "compare" one_term one_term | "rewrite_strat" rewstrategy "in" ident | "intros" intropattern_list_opt | "eintros" intropattern_list_opt @@ -1536,41 +1532,43 @@ simple_tactic: [ | "fix" ident num "with" LIST1 fixdecl | "cofix" ident "with" LIST1 cofixdecl | "pose" bindings_with_parameters -| "pose" term1_extended as_name +| "pose" one_term as_name | "epose" bindings_with_parameters -| "epose" term1_extended as_name +| "epose" one_term as_name | "set" bindings_with_parameters clause_dft_concl -| "set" term1_extended as_name clause_dft_concl +| "set" one_term as_name clause_dft_concl | "eset" bindings_with_parameters clause_dft_concl -| "eset" term1_extended as_name clause_dft_concl -| "remember" term1_extended as_name eqn_ipat clause_dft_all -| "eremember" term1_extended as_name eqn_ipat clause_dft_all +| "eset" one_term as_name clause_dft_concl +| "remember" one_term as_name eqn_ipat clause_dft_all +| "eremember" one_term as_name eqn_ipat clause_dft_all | "assert" "(" ident ":=" term ")" | "eassert" "(" ident ":=" term ")" | "assert" "(" ident ":" term ")" by_tactic | "eassert" "(" ident ":" term ")" by_tactic | "enough" "(" ident ":" term ")" by_tactic | "eenough" "(" ident ":" term ")" by_tactic -| "assert" term1_extended as_ipat by_tactic -| "eassert" term1_extended as_ipat by_tactic +| "assert" one_term as_ipat by_tactic +| "eassert" one_term as_ipat by_tactic +| "pose" "proof" "(" ident ":=" term ")" +| "epose" "proof" "(" ident ":=" term ")" | "pose" "proof" term as_ipat | "epose" "proof" term as_ipat -| "enough" term1_extended as_ipat by_tactic -| "eenough" term1_extended as_ipat by_tactic -| "generalize" term1_extended -| "generalize" term1_extended LIST1 term1_extended -| "generalize" term1_extended OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ] +| "enough" one_term as_ipat by_tactic +| "eenough" one_term as_ipat by_tactic +| "generalize" one_term +| "generalize" one_term LIST1 one_term +| "generalize" one_term OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ] | "induction" induction_clause_list | "einduction" induction_clause_list | "destruct" induction_clause_list | "edestruct" induction_clause_list | "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic | "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic -| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" term1_extended ] +| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" one_term ] | "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list | "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list | "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list -| "inversion" quantified_hypothesis "using" term1_extended in_hyp_list +| "inversion" quantified_hypothesis "using" one_term in_hyp_list | "red" clause_dft_concl | "hnf" clause_dft_concl | "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl @@ -1581,7 +1579,7 @@ simple_tactic: [ | "vm_compute" OPT ref_or_pattern_occ clause_dft_concl | "native_compute" OPT ref_or_pattern_occ clause_dft_concl | "unfold" LIST1 unfold_occ SEP "," clause_dft_concl -| "fold" LIST1 term1_extended clause_dft_concl +| "fold" LIST1 one_term clause_dft_concl | "pattern" LIST1 pattern_occ SEP "," clause_dft_concl | "change" conversion clause_dft_concl | "change_no_check" conversion clause_dft_concl @@ -1589,16 +1587,16 @@ simple_tactic: [ | "rtauto" | "congruence" | "congruence" int -| "congruence" "with" LIST1 term1_extended -| "congruence" int "with" LIST1 term1_extended +| "congruence" "with" LIST1 one_term +| "congruence" int "with" LIST1 one_term | "f_equal" | "firstorder" OPT ltac_expr firstorder_using | "firstorder" OPT ltac_expr "with" LIST1 ident | "firstorder" OPT ltac_expr firstorder_using "with" LIST1 ident | "gintuition" OPT ltac_expr | "functional" "inversion" quantified_hypothesis OPT qualid (* funind plugin *) -| "functional" "induction" LIST1 term1_extended fun_ind_using with_names (* funind plugin *) -| "soft" "functional" "induction" LIST1 term1_extended fun_ind_using with_names (* funind plugin *) +| "functional" "induction" LIST1 one_term fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" LIST1 one_term fun_ind_using with_names (* funind plugin *) | "psatz_Z" int_or_var ltac_expr (* micromega plugin *) | "psatz_Z" ltac_expr (* micromega plugin *) | "xlia" ltac_expr (* micromega plugin *) @@ -1614,16 +1612,17 @@ simple_tactic: [ | "psatz_R" ltac_expr (* micromega plugin *) | "psatz_Q" int_or_var ltac_expr (* micromega plugin *) | "psatz_Q" ltac_expr (* micromega plugin *) -| "zify_iter_specs" ltac_expr (* micromega plugin *) +| "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) | "zify_saturate" (* micromega plugin *) | "zify_iter_let" ltac_expr (* micromega plugin *) -| "nsatz_compute" term1_extended (* nsatz plugin *) +| "zify_elim_let" (* micromega plugin *) +| "nsatz_compute" one_term (* nsatz plugin *) | "omega" (* omega plugin *) | "protect_fv" string "in" ident (* setoid_ring plugin *) | "protect_fv" string (* setoid_ring plugin *) -| "ring_lookup" ltac_expr0 "[" LIST0 term1_extended "]" LIST1 term1_extended (* setoid_ring plugin *) -| "field_lookup" ltac_expr "[" LIST0 term1_extended "]" LIST1 term1_extended (* setoid_ring plugin *) +| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *) +| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *) ] hloc: [ @@ -1646,11 +1645,23 @@ by_arg_tac: [ ] in_clause: [ -| in_clause +| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ ) +| "*" "|-" OPT concl_occ | "*" OPT ( "at" occs_nums ) -| "*" "|-" concl_occ -| LIST0 hypident_occ SEP "," "|-" concl_occ -| LIST0 hypident_occ SEP "," +] + +concl_occ: [ +| "*" OPT ( "at" occs_nums ) +] + +hypident_occ: [ +| hypident OPT ( "at" occs_nums ) +] + +hypident: [ +| ident +| "(" "type" "of" ident ")" +| "(" "value" "of" ident ")" ] as_ipat: [ @@ -1707,7 +1718,7 @@ induction_clause_list: [ ] auto_using: [ -| "using" LIST1 term1_extended SEP "," +| "using" LIST1 one_term SEP "," | ] @@ -1762,7 +1773,7 @@ simple_binding: [ bindings: [ | LIST1 simple_binding -| LIST1 term1_extended +| LIST1 one_term ] comparison: [ @@ -1783,16 +1794,6 @@ bindings_with_parameters: [ | "(" ident LIST0 simple_binder ":=" term ")" ] -hypident: [ -| ident -| "(" "type" "of" ident ")" -| "(" "value" "of" ident ")" -] - -hypident_occ: [ -| hypident OPT ( "at" occs_nums ) -] - clause_dft_concl: [ | "in" in_clause | OPT ( "at" occs_nums ) @@ -1810,11 +1811,6 @@ opt_clause: [ | ] -concl_occ: [ -| "*" OPT ( "at" occs_nums ) -| -] - in_hyp_list: [ | "in" LIST1 ident | @@ -1844,7 +1840,7 @@ cofixdecl: [ ] constr_with_bindings: [ -| term1_extended with_bindings +| one_term with_bindings ] with_bindings: [ @@ -1869,9 +1865,9 @@ quantified_hypothesis: [ ] conversion: [ -| term1_extended -| term1_extended "with" term1_extended -| term1_extended "at" occs_nums "with" term1_extended +| one_term +| one_term "with" one_term +| one_term "at" occs_nums "with" one_term ] firstorder_using: [ @@ -1897,29 +1893,29 @@ occurrences: [ ] rewstrategy: [ -| term1_extended -| "<-" term1_extended -| "subterms" rewstrategy -| "subterm" rewstrategy -| "innermost" rewstrategy -| "outermost" rewstrategy -| "bottomup" rewstrategy -| "topdown" rewstrategy -| "id" +| one_term +| "<-" one_term | "fail" +| "id" | "refl" | "progress" rewstrategy | "try" rewstrategy -| "any" rewstrategy -| "repeat" rewstrategy | rewstrategy ";" rewstrategy -| "(" rewstrategy ")" | "choice" rewstrategy rewstrategy -| "old_hints" ident +| "repeat" rewstrategy +| "any" rewstrategy +| "subterm" rewstrategy +| "subterms" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy | "hints" ident -| "terms" LIST0 term1_extended +| "terms" LIST0 one_term | "eval" red_expr -| "fold" term1_extended +| "fold" one_term +| "(" rewstrategy ")" +| "old_hints" ident ] ltac_expr: [ @@ -2037,7 +2033,7 @@ tactic_arg: [ | "context" ident "[" term "]" | "type" "of" term | "fresh" LIST0 fresh_id -| "type_term" term1_extended +| "type_term" one_term | "numgoals" ] diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg index 37197a1fec..8bd8cad6b5 100644 --- a/doc/tools/docgram/prodn.edit_mlg +++ b/doc/tools/docgram/prodn.edit_mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg index 93eb38d1a0..641ab8fbe5 100644 --- a/doc/tools/docgram/productionlist.edit_mlg +++ b/doc/tools/docgram/productionlist.edit_mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |