diff options
Diffstat (limited to 'doc')
41 files changed, 702 insertions, 750 deletions
diff --git a/doc/changelog/03-notations/13840-print-prim.rst b/doc/changelog/03-notations/13840-print-prim.rst new file mode 100644 index 0000000000..d6e3184662 --- /dev/null +++ b/doc/changelog/03-notations/13840-print-prim.rst @@ -0,0 +1,11 @@ +- **Changed:** + Flag :flag:`Printing Notations` no longer controls + whether strings and numbers are printed raw + (`#13840 <https://github.com/coq/coq/pull/13840>`_, + by Enrico Tassi). + +- **Added:** + Flag :flag:`Printing Raw Literals` to control whether + strings and numbers are printed raw. + (`#13840 <https://github.com/coq/coq/pull/13840>`_, + by Enrico Tassi). diff --git a/doc/changelog/04-tactics/13741-remove_omega.rst b/doc/changelog/04-tactics/13741-remove_omega.rst new file mode 100644 index 0000000000..0b25c01958 --- /dev/null +++ b/doc/changelog/04-tactics/13741-remove_omega.rst @@ -0,0 +1,7 @@ +- **Removed:** + Removed the `omega` tactic (deprecated in 8.12) and 4 `* Omega *` flags. + Use `lia` instead. + (`#13741 <https://github.com/coq/coq/pull/13741>`_, + by Jim Fehrle, who addressed the final details, building on much work by + Frédéric Besson, who greatly improved :tacn:`lia`, Maxime Dénès, + Vincent Laporte and with the help of many package maintainers, among others). diff --git a/doc/changelog/04-tactics/14033-fix-14009.rst b/doc/changelog/04-tactics/14033-fix-14009.rst new file mode 100644 index 0000000000..3b58e193cb --- /dev/null +++ b/doc/changelog/04-tactics/14033-fix-14009.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Properly expand projection parameters in hint discrimination + nets. (`#14033 <https://github.com/coq/coq/pull/14033>`_, + fixes `#9000 <https://github.com/coq/coq/issues/9000>`_, + `#14009 <https://github.com/coq/coq/issues/14009>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst b/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst new file mode 100644 index 0000000000..5fdfbd9796 --- /dev/null +++ b/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst @@ -0,0 +1,6 @@ +- **Added:** + Ltac2 commands defining terms now accept the :attr:`deprecated` + attribute + (`#13774 <https://github.com/coq/coq/pull/13774>`_, + fixes `#12317 <https://github.com/coq/coq/issues/12317>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst b/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst new file mode 100644 index 0000000000..5ecc5934eb --- /dev/null +++ b/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst @@ -0,0 +1,5 @@ +- **Added:** + Allow the presence of type casts for function return values, let bindings and + global definitions in Ltac2 + (`#13914 <https://github.com/coq/coq/pull/13914>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst b/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst new file mode 100644 index 0000000000..32499957be --- /dev/null +++ b/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst @@ -0,0 +1,5 @@ +- **Added:** + Added the Ltac2 API `Ltac2.Ind` for manipulating inductive types + (`#13920 <https://github.com/coq/coq/pull/13920>`_, + fixes `#10095 <https://github.com/coq/coq/issues/10095>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst new file mode 100644 index 0000000000..9753ce915b --- /dev/null +++ b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst @@ -0,0 +1,5 @@ +- **Added:** + Allow scope delimiters in Ltac2 open_constr:(...) quotation + (`#13939 <https://github.com/coq/coq/pull/13939>`_, + fixes `#12806 <https://github.com/coq/coq/issues/12806>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst b/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst new file mode 100644 index 0000000000..b5b63455c9 --- /dev/null +++ b/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst @@ -0,0 +1,5 @@ +- **Added:** + Added a FFI to convert between Ltac1 and Ltac2 identifiers + (`#13997 <https://github.com/coq/coq/pull/13997>`_, + fixes `#13996 <https://github.com/coq/coq/issues/13996>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst b/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst new file mode 100644 index 0000000000..d3ef244cb0 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst @@ -0,0 +1,6 @@ +- **Changed:** + In `Record`, alpha-rename the variable associated with the record to avoid + alpha-renaming parameters of projections + (`#13852 <https://github.com/coq/coq/pull/13852>`_, + fixes `#13727 <https://github.com/coq/coq/issues/13727>`_, + by Li-yao Xia). diff --git a/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst b/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst new file mode 100644 index 0000000000..c5a2172005 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst @@ -0,0 +1,6 @@ +- **Changed:** + Improve the :cmd:`Coercion` command to reduce the number of ambiguous paths to + report. A pair of multiple inheritance paths that can be reduced to smaller + adjoining pairs will not be reported as ambiguous paths anymore. + (`#13909 <https://github.com/coq/coq/pull/13909>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/changelog/07-vernac-commands-and-options/13912-remove-bijint.rst b/doc/changelog/07-vernac-commands-and-options/13912-remove-bijint.rst new file mode 100644 index 0000000000..99efda3a5b --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13912-remove-bijint.rst @@ -0,0 +1,5 @@ +- **Changed:** + The printing order of :cmd:`Print Classes` and :cmd:`Print Graph`, due to the + changes for the internal tables of coercion classes and coercion paths. + (`#13912 <https://github.com/coq/coq/pull/13912>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst new file mode 100644 index 0000000000..7831d10392 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 grammar can now be printed using the + Print Grammar ltac2 command + (`#14093 <https://github.com/coq/coq/pull/14093>`_, + fixes `#14092 <https://github.com/coq/coq/issues/14092>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst new file mode 100644 index 0000000000..6a34f5a70e --- /dev/null +++ b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Failure of extraction in the presence of inductive types with local + definitions in parameters + (`#13624 <https://github.com/coq/coq/pull/13624>`_, + fixes `#13581 <https://github.com/coq/coq/issues/13581>`_, + by Hugo Herbelin). diff --git a/doc/changelog/08-cli-tools/14024-coqdep-errors.rst b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst new file mode 100644 index 0000000000..355c0bd7b7 --- /dev/null +++ b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst @@ -0,0 +1,8 @@ +- **Changed:** + ``coqdep`` now reports an error if files specified on the + command line don't exist or if it encounters unreadable files. + Unknown options now generate a warning. Previously these + conditions were ignored. + (`#14024 <https://github.com/coq/coq/pull/14024>`_, + fixes `#14023 <https://github.com/coq/coq/issues/14023>`_, + by Hendrik Tews). diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst index 27d89b2f8b..ff4e8db8b0 100644 --- a/doc/changelog/10-standard-library/13582-exp_ineq.rst +++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst @@ -4,6 +4,4 @@ Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). (`#13582 <https://github.com/coq/coq/pull/13582>`_, - by Avi Shinnar and Barry Trager, with help from Laurent Théry - -). + by Avi Shinnar and Barry Trager, with help from Laurent Théry). diff --git a/doc/changelog/10-standard-library/13671-Vector_to_list.rst b/doc/changelog/10-standard-library/13671-Vector_to_list.rst new file mode 100644 index 0000000000..e8404f0c93 --- /dev/null +++ b/doc/changelog/10-standard-library/13671-Vector_to_list.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas about vectors related with ``to_list``: ``length_to_list``, ``of_list_to_list_opp``, ``to_list_nil``, ``to_list_cons``, ``to_list_hd``, ``to_list_last``, ``to_list_const``, ``to_list_nth_order``, ``to_list_tl``, ``to_list_append``, ``to_list_rev_append_tail``, ``to_list_rev_append``, ``to_list_rev``, ``to_list_map``, ``to_list_fold_left``, ``to_list_fold_right``, ``to_list_Forall``, ``to_list_Exists``, ``to_list_In``, ``to_list_Forall2`` + (`#13671 <https://github.com/coq/coq/pull/13671>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/13804-count_occ.rst b/doc/changelog/10-standard-library/13804-count_occ.rst new file mode 100644 index 0000000000..9354b219d8 --- /dev/null +++ b/doc/changelog/10-standard-library/13804-count_occ.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas about ``count_occ``: ``count_occ_app``, ``count_occ_elt_eq``, ``count_occ_elt_neq``, ``count_occ_bound``, ``count_occ_repeat_eq``, ``count_occ_repeat_neq``, ``count_occ_unique``, ``count_occ_repeat_excl``, ``count_occ_sgt``, ``Permutation_count_occ`` + (`#13804 <https://github.com/coq/coq/pull/13804>`_, + by Olivier Laurent with help of Jean-Christophe Léchenet). diff --git a/doc/changelog/10-standard-library/13955-List_lemmas1.rst b/doc/changelog/10-standard-library/13955-List_lemmas1.rst new file mode 100644 index 0000000000..73eb9a78d9 --- /dev/null +++ b/doc/changelog/10-standard-library/13955-List_lemmas1.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas to ``List``: ``Exists_map``, ``Exists_concat``, ``Exists_flat_map``, ``Forall_map``, ``Forall_concat``, ``Forall_flat_map``, ``nth_error_map``, ``nth_repeat``, ``nth_error_repeat`` + (`#13955 <https://github.com/coq/coq/pull/13955>`_, + by Andrej Dudenhefner, with help from Olivier Laurent). diff --git a/doc/changelog/10-standard-library/13986-clean-List-imports.rst b/doc/changelog/10-standard-library/13986-clean-List-imports.rst new file mode 100644 index 0000000000..02e7b9cc97 --- /dev/null +++ b/doc/changelog/10-standard-library/13986-clean-List-imports.rst @@ -0,0 +1,4 @@ +- **Removed:** + from ``List.v`` deprecated/unexpected dependencies ``Setoid``, ``Le``, ``Gt``, ``Minus``, ``Lt`` + (`#13986 <https://github.com/coq/coq/pull/13986>`_, + by Andrej Dudenhefner). diff --git a/doc/changelog/10-standard-library/14008-Cantor-pairing.rst b/doc/changelog/10-standard-library/14008-Cantor-pairing.rst new file mode 100644 index 0000000000..4c217f3fb0 --- /dev/null +++ b/doc/changelog/10-standard-library/14008-Cantor-pairing.rst @@ -0,0 +1,6 @@ +- **Added:** + ``Cantor.v`` containing the Cantor pairing function and its inverse. + ``Cantor.to_nat : nat * nat -> nat`` and ``Cantor.of_nat : nat -> nat * nat`` + are the respective bijections between ``nat * nat`` and ``nat``. + (`#14008 <https://github.com/coq/coq/pull/14008>`_, + by Andrej Dudenhefner). @@ -63,3 +63,6 @@ (files (refman-html as html/refman) (refman-pdf as pdf/refman)) (section doc) (package coq-doc)) + +(documentation + (package coq-doc)) diff --git a/doc/index.mld b/doc/index.mld new file mode 100644 index 0000000000..3a1979bc62 --- /dev/null +++ b/doc/index.mld @@ -0,0 +1,3 @@ +{0 coq-doc } + +The coq-doc package only contains user documentation on the Coq proof assistant and no OCaml library. diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index 2a618f68d2..a4850a738b 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -69,7 +69,7 @@ } .ansi-fg-white { - color: #2e3436; + color: #ffffff; } .ansi-fg-light-black { diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 5d471c695c..d718454364 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -159,7 +159,6 @@ and checked to be :math:`-1`. This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. - High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst deleted file mode 100644 index 86bb0502c6..0000000000 --- a/doc/sphinx/addendum/omega.rst +++ /dev/null @@ -1,210 +0,0 @@ -.. _omega_chapter: - -Omega: a (deprecated) solver for arithmetic -===================================================================== - -:Author: Pierre Crégut - -.. warning:: - - The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia` - tactic. The goal is to consolidate the arithmetic solving - capabilities of Coq into a single engine; moreover, :tacn:`lia` is - in general more powerful than :tacn:`omega` (it is a complete - Presburger arithmetic solver while :tacn:`omega` was known to be - incomplete). - - It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing - projects. We also ask that you report (in our `bug tracker - <https://github.com/coq/coq/issues>`_) any issue you encounter, especially - if the issue was not present in :tacn:`omega`. If no new issues are - reported, :tacn:`omega` will be removed soon. - - Note that replacing :tacn:`omega` with :tacn:`lia` can break - non-robust proof scripts which rely on incompleteness bugs of - :tacn:`omega` (e.g. using the pattern :g:`; try omega`). - -Description of ``omega`` ------------------------- - -.. tacn:: omega - - .. deprecated:: 8.12 - - Use :tacn:`lia` instead. - - :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, - i.e. for proving formulas made of equations and inequalities over the - type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers. - Formulas on ``nat`` are automatically injected into ``Z``. The procedure - may use any hypothesis of the current proof session to solve the goal. - - Multiplication is handled by :tacn:`omega` but only goals where at - least one of the two multiplicands of products is a constant are - solvable. This is the restriction meant by "Presburger arithmetic". - - If the tactic cannot solve the goal, it fails with an error message. - In any case, the computation eventually stops. - -Arithmetical goals recognized by ``omega`` ------------------------------------------- - -:tacn:`omega` applies only to quantifier-free formulas built from the connectives:: - - /\ \/ ~ -> - -on atomic formulas. Atomic formulas are built from the predicates:: - - = < <= > >= - -on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes:: - - + - * S O pred - -and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and:: - - + - * Z.succ Z.pred - -All expressions of type ``nat`` or ``Z`` not built on these -operators are considered abstractly as if they -were arbitrary variables of type ``nat`` or ``Z``. - -Messages from ``omega`` ------------------------ - -When :tacn:`omega` does not solve the goal, one of the following errors -is generated: - -.. exn:: omega can't solve this system. - - This may happen if your goal is not quantifier-free (if it is - universally quantified, try :tacn:`intros` first; if it contains - existentials quantifiers too, :tacn:`omega` is not strong enough to solve your - goal). This may happen also if your goal contains arithmetical - operators not recognized by :tacn:`omega`. Finally, your goal may be simply - not true! - -.. exn:: omega: Not a quantifier-free goal. - - If your goal is universally quantified, you should first apply - :tacn:`intro` as many times as needed. - -.. exn:: omega: Unrecognized predicate or connective: @ident. - :undocumented: - -.. exn:: omega: Unrecognized atomic proposition: ... - :undocumented: - -.. exn:: omega: Can't solve a goal with proposition variables. - :undocumented: - -.. exn:: omega: Unrecognized proposition. - :undocumented: - -.. exn:: omega: Can't solve a goal with non-linear products. - :undocumented: - -.. exn:: omega: Can't solve a goal with equality on type ... - :undocumented: - - -Using ``omega`` ---------------- - -The ``omega`` tactic does not belong to the core system. It should be -loaded by - -.. coqtop:: in - - Require Import Omega. - -.. example:: - - .. coqtop:: all warn - - Require Import Omega. - - Open Scope Z_scope. - - Goal forall m n:Z, 1 + 2 * m <> 2 * n. - intros; omega. - Abort. - - Goal forall z:Z, z > 0 -> 2 * z + 1 > z. - intro; omega. - Abort. - - -Options -------- - -.. flag:: Stable Omega - - .. deprecated:: 8.5 - - This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It - resets internal name counters to make executions of :tacn:`omega` independent. - -.. flag:: Omega UseLocalDefs - - This flag (on by default) allows :tacn:`omega` to use the :term:`bodies <body>` of local - variables. - -.. flag:: Omega System - - This flag (off by default) activate the printing of debug information - -.. flag:: Omega Action - - This flag (off by default) activate the printing of debug information - -Technical data --------------- - -Overview of the tactic -~~~~~~~~~~~~~~~~~~~~~~ - - * The goal is negated twice and the first negation is introduced as a hypothesis. - * Hypotheses are decomposed in simple equations or inequalities. Multiple - goals may result from this phase. - * Equations and inequalities over ``nat`` are translated over - ``Z``, multiple goals may result from the translation of subtraction. - * Equations and inequalities are normalized. - * Goals are solved by the OMEGA decision procedure. - * The script of the solution is replayed. - -Overview of the OMEGA decision procedure -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The OMEGA decision procedure involved in the :tacn:`omega` tactic uses -a small subset of the decision procedure presented in :cite:`TheOmegaPaper` -Here is an overview, refer to the original paper for more information. - - * Equations and inequalities are normalized by division by the GCD of their - coefficients. - * Equations are eliminated, using the Banerjee test to get a coefficient - equal to one. - * Note that each inequality cuts the Euclidean space in half. - * Inequalities are solved by projecting on the hyperspace - defined by cancelling one of the variables. They are partitioned - according to the sign of the coefficient of the eliminated - variable. Pairs of inequalities from different classes define a - new edge in the projection. - * Redundant inequalities are eliminated or merged in new - equations that can be eliminated by the Banerjee test. - * The last two steps are iterated until a contradiction is reached - (success) or there is no more variable to eliminate (failure). - -It may happen that there is a real solution and no integer one. The last -steps of the Omega procedure are not implemented, so the -decision procedure is only partial. - -Bugs ----- - - * The simplification procedure is very dumb and this results in - many redundant cases to explore. - - * Much too slow. - - * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 4f3ee2dcaf..f8d6b35226 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -721,6 +721,33 @@ CoqIDE (`#13870 <https://github.com/coq/coq/pull/13870>`_, by Guillaume Melquiond). +Changes in 8.13.2 +~~~~~~~~~~~~~~~~~ + +Kernel +^^^^^^ + +- **Fixed:** + Crash when using :tacn:`vm_compute` on an irreducible ``PArray.set`` + (`#14005 <https://github.com/coq/coq/pull/14005>`_, + fixes `#13998 <https://github.com/coq/coq/issues/13998>`_, + by Guillaume Melquiond). +- **Fixed:** + Never store persistent arrays as VM / native structured values. + This could be used to make vo marshalling crash, and probably + breaking some other invariants of the kernel + (`#14007 <https://github.com/coq/coq/pull/14007>`_, + fixes `#14006 <https://github.com/coq/coq/issues/14006>`_, + by Pierre-Marie Pédrot). + +Tactic language +^^^^^^^^^^^^^^^^ + +- **Fixed:** + Ltac2 ``Array.init`` no longer incurs exponential overhead when used + recursively (`#14012 <https://github.com/coq/coq/pull/14012>`_, fixes `#14011 + <https://github.com/coq/coq/issues/14011>`_, by Jason Gross). + Version 8.12 ------------ @@ -751,10 +778,8 @@ The main changes include: of chapters along with updated syntax descriptions that match Coq's grammar in most but not all chapters. -Additionally, the :tacn:`omega` tactic is deprecated in this version of Coq, -and we recommend users to switch to :tacn:`lia` in new proof scripts (see -also the warning message in the :ref:`corresponding chapter -<omega_chapter>`). +Additionally, the `omega` tactic is deprecated in this version of Coq, +and we recommend users to switch to :tacn:`lia` in new proof scripts. See the `Changes in 8.12+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked @@ -1019,7 +1044,7 @@ Tactics <https://github.com/coq/coq/pull/10760>`_, by Jason Gross). - **Changed:** The :g:`auto with zarith` tactic and variations (including - :tacn:`intuition`) may now call :tacn:`lia` instead of :tacn:`omega` + :tacn:`intuition`) may now call :tacn:`lia` instead of `omega` (when the `Omega` module is loaded); more goals may be automatically solved, fewer section variables will be captured spuriously (`#11018 <https://github.com/coq/coq/pull/11018>`_, @@ -1115,7 +1140,7 @@ Tactics (`#11883 <https://github.com/coq/coq/pull/11883>`_, by Attila Gáspár). - **Deprecated:** - The :tacn:`omega` tactic is deprecated; + The `omega` tactic is deprecated; use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead (`#11976 <https://github.com/coq/coq/pull/11976>`_, by Vincent Laporte). @@ -2102,11 +2127,9 @@ The main changes brought by Coq version 8.11 are: - :ref:`Revision<811Reals>` of the :g:`Coq.Reals` library, its axiomatisation and instances of the constructive and classical real numbers. -Additionally, while the :tacn:`omega` tactic is not yet deprecated in +Additionally, while the `omega` tactic is not yet deprecated in this version of Coq, it should soon be the case and we already -recommend users to switch to :tacn:`lia` in new proof scripts (see -also the warning message in the :ref:`corresponding chapter -<omega_chapter>`). +recommend users to switch to :tacn:`lia` in new proof scripts. The ``dev/doc/critical-bugs`` file documents the known critical bugs of Coq and affected releases. See the `Changes in 8.11+beta1`_ diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 9f097b4fe9..abe928fa26 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -5,7 +5,7 @@ The underlying formal language of Coq is a :gdef:`Calculus of Inductive Constructions` (|Cic|) whose inference rules are presented in this chapter. The history of this formalism as well as pointers to related -work are provided in a separate chapter; see *Credits*. +work are provided in a separate chapter; see :ref:`history`. .. _The-terms: diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5d36ec3cf9..49c2c6b785 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -515,6 +515,11 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target (``.PHONY`` or not) please use ``CoqMakefile.local``. +.. note:: + + Due to limitations with the compilation chain, makefiles generated + by ``coq_makefile`` won't correctly compile OCaml plugins with OCaml + < 4.07.0 when using more than one job (``-j N`` for ``N > 1``). Precompiling for ``native_compute`` +++++++++++++++++++++++++++++++++++ diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b1759bf71b..88fca93547 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1666,7 +1666,7 @@ Proving a subgoal as a separate lemma: abstract is chosen to get a fresh name. If the proof is closed with :cmd:`Qed`, the auxiliary lemma is inlined in the final proof term. - This is useful with tactics such as :tacn:`omega` or + This is useful with tactics such as :tacn:`discriminate` that generate huge proof terms with many intermediate goals. It can significantly reduce peak memory use. In most cases it doesn't have a significant impact on run time. One case in which it can reduce run time @@ -2317,11 +2317,10 @@ performance issue. .. coqtop:: reset in - Set Warnings "-omega-is-deprecated". - Require Import Coq.omega.Omega. + Require Import Lia. Ltac mytauto := tauto. - Ltac tac := intros; repeat split; omega || mytauto. + Ltac tac := intros; repeat split; lia || mytauto. Notation max x y := (x + (y - x)) (only parsing). @@ -2340,7 +2339,7 @@ performance issue. Set Ltac Profiling. tac. Show Ltac Profile. - Show Ltac Profile "omega". + Show Ltac Profile "lia". .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 9f3f0ef3d5..25ac72069b 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -66,7 +66,6 @@ Current limitations include: - An easy way to get the number of constructors of an inductive type. Currently only way to do this is to destruct a variable of the inductive type and count the number of goals that result. -- The :attr:`deprecated` attribute is not supported for Ltac2 definitions. - Error messages may be cryptic. @@ -229,6 +228,8 @@ One can define new types with the following commands. defined in Coq and give their type information. They can also declare data structures from OCaml. This command has no use for the end user. + This command supports the :attr:`deprecated` attribute. + APIs ~~~~ @@ -263,10 +264,10 @@ There is dedicated syntax for list and array literals. .. prodn:: ltac2_expr ::= @ltac2_expr5 ; @ltac2_expr | @ltac2_expr5 - ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr + ltac2_expr5 ::= fun {+ @tac2pat0 } {? : @ltac2_type } => @ltac2_expr | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr | @ltac2_expr3 - ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr + ltac2_let_clause ::= {+ @tac2pat0 } {? : @ltac2_type } := @ltac2_expr ltac2_expr3 ::= {+, @ltac2_expr2 } ltac2_expr2 ::= @ltac2_expr1 :: @ltac2_expr2 | @ltac2_expr1 @@ -304,7 +305,7 @@ Ltac2 Definitions .. insertprodn tac2def_body tac2def_body .. prodn:: - tac2def_body ::= {| _ | @ident } {* @tac2pat0 } := @ltac2_expr + tac2def_body ::= {| _ | @ident } {* @tac2pat0 } {? : @ltac2_type } := @ltac2_expr This command defines a new global Ltac2 value. If one or more :token:`tac2pat0` are specified, the new value is a function. This is a shortcut for one of the @@ -319,6 +320,8 @@ Ltac2 Definitions If ``mutable`` is set, the definition can be redefined at a later stage (see below). + This command supports the :attr:`deprecated` attribute. + .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr This command redefines a previous ``mutable`` definition. @@ -1246,6 +1249,8 @@ Notations so that you may have to resort to thunking to ensure that side-effects are performed at the right time. + This command supports the :attr:`deprecated` attribute. + Abbreviations ~~~~~~~~~~~~~ @@ -1276,6 +1281,8 @@ Abbreviations Note that abbreviations are not type checked at all, and may result in typing errors after expansion. + This command supports the :attr:`deprecated` attribute. + .. _defining_tactics: Defining tactics @@ -1368,8 +1375,9 @@ table further down lists the classes that that are handled plainly. the term (as described in :ref:`LocalInterpretationRulesForNotations`). The last :token:`scope_key` is the top of the scope stack that's applied to the :token:`term`. - :n:`open_constr` - Parses an open :token:`term`. + :n:`open_constr {? ( {+, @scope_key } ) }` + Parses an open :token:`term`. Like :n:`constr` above, this class + accepts a list of notation scopes with the same effects. :n:`ident` Parses :token:`ident` or :n:`$@ident`. The first form returns :n:`ident:(@ident)`, diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst index c3712b109d..e458c3a9f5 100644 --- a/doc/sphinx/proofs/automatic-tactics/index.rst +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -14,7 +14,6 @@ complex goals in new domains. :maxdepth: 1 logic - ../../addendum/omega ../../addendum/micromega ../../addendum/ring ../../addendum/nsatz diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 557ef10555..d212256765 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -442,6 +442,12 @@ Displaying information about notations Controls whether to use notations for printing terms wherever possible. Default is on. +.. flag:: Printing Raw Literals + + Controls whether to use string and number notations for printing terms + wherever possible (see :ref:`string-notations`). + Default is off. + .. flag:: Printing Parentheses If on, parentheses are printed even if implied by associativity and precedence @@ -461,6 +467,7 @@ Displaying information about notations - `tactic` - for currently-defined tactic notations, :token:`tactic`\s and tacticals (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s + - `ltac2` - for Ltac2 notations (corresponding to :token:`ltac2_expr`) This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 917edf0774..7461bfe443 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -22,13 +22,17 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` by a comma. This attribute is supported by the following commands: :cmd:`Ltac`, - :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`, + :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`. It can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string__since. @string__note. Tactic Notation @qualid is deprecated since @string__since. @string__note. Notation @string is deprecated since @string__since. @string__note. + Ltac2 definition @qualid is deprecated since @string__since. @string__note. + Ltac2 alias @qualid is deprecated since @string__since. @string__note. + Ltac2 notation {+ @ltac2_scope } is deprecated since @string__since. @string__note. :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number, :n:`@string__note` is diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index e4f0967794..bca66cc61b 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -58,10 +58,7 @@ theories/micromega/ZifyPow.v theories/micromega/Zify.v theories/nsatz/NsatzTactic.v theories/nsatz/Nsatz.v -theories/omega/Omega.v theories/omega/OmegaLemmas.v -theories/omega/OmegaPlugin.v -theories/omega/OmegaTactic.v theories/omega/PreOmega.v theories/quote/Quote.v theories/romega/ROmega.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index b0f4e883be..6fda3b06ce 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -135,6 +135,7 @@ through the <tt>Require Import</tt> command.</p> theories/Arith/Bool_nat.v theories/Arith/Factorial.v theories/Arith/Wf_nat.v + theories/Arith/Cantor.v </dd> <dt> <b>PArith</b>: @@ -685,6 +686,7 @@ through the <tt>Require Import</tt> command.</p> user-contrib/Ltac2/Fresh.v user-contrib/Ltac2/Ident.v user-contrib/Ltac2/Init.v + user-contrib/Ltac2/Ind.v user-contrib/Ltac2/Int.v user-contrib/Ltac2/List.v user-contrib/Ltac2/Ltac1.v diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1ab4fe8f81..aa95d4f249 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -529,12 +529,12 @@ class ProductionObject(CoqObject): self.signatures = [] indexnode = super().run()[0] # makes calls to handle_signature - table = nodes.container(classes=['prodn-table']) - tgroup = nodes.container(classes=['prodn-column-group']) + table = nodes.inline(classes=['prodn-table']) + tgroup = nodes.inline(classes=['prodn-column-group']) for _ in range(4): - tgroup += nodes.container(classes=['prodn-column']) + tgroup += nodes.inline(classes=['prodn-column']) table += tgroup - tbody = nodes.container(classes=['prodn-row-group']) + tbody = nodes.inline(classes=['prodn-row-group']) table += tbody # create rows @@ -542,8 +542,8 @@ class ProductionObject(CoqObject): lhs, op, rhs, tag = signature position = self.state_machine.get_source_and_line(self.lineno) - row = nodes.container(classes=['prodn-row']) - entry = nodes.container(classes=['prodn-cell-nonterminal']) + row = nodes.inline(classes=['prodn-row']) + entry = nodes.inline(classes=['prodn-cell-nonterminal']) if lhs != "": target_name = make_id('grammar-token-' + lhs) target = nodes.target('', '', ids=[target_name], names=[target_name]) @@ -553,19 +553,19 @@ class ProductionObject(CoqObject): entry += inline entry += notation_to_sphinx('@'+lhs, *position) else: - entry += nodes.Text('') + entry += nodes.literal('', '') row += entry - entry = nodes.container(classes=['prodn-cell-op']) - entry += nodes.Text(op) + entry = nodes.inline(classes=['prodn-cell-op']) + entry += nodes.literal(op, op) row += entry - entry = nodes.container(classes=['prodn-cell-production']) + entry = nodes.inline(classes=['prodn-cell-production']) entry += notation_to_sphinx(rhs, *position) row += entry - entry = nodes.container(classes=['prodn-cell-tag']) - entry += nodes.Text(tag) + entry = nodes.inline(classes=['prodn-cell-tag']) + entry += nodes.literal(tag, tag) row += entry tbody += row diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py index 9e23be2409..6700c20b1a 100644 --- a/doc/tools/coqrst/repl/ansicolors.py +++ b/doc/tools/coqrst/repl/ansicolors.py @@ -91,7 +91,10 @@ def parse_ansi(code): leading ‘^[[’ or the final ‘m’ """ classes = [] - parse_style([int(c) for c in code.split(';')], 0, classes) + if code == "37": + pass # ignore white fg + else: + parse_style([int(c) for c in code.split(';')], 0, classes) return ["ansi-" + cls for cls in classes] if __name__ == '__main__': diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 24ecc65e9b..fd1c3c0260 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -2730,6 +2730,7 @@ SPLICE: [ | variance_identref | rewriter | conversion +| type_cast ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 4ba60ddd9f..873b2f8dff 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -21,7 +21,6 @@ (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/ring/*.mlg) (glob_files %{project_root}/plugins/rtauto/*.mlg) (glob_files %{project_root}/plugins/ssr/*.mlg) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index be1b9d80fb..0c8980b1bd 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1,6 +1,492 @@ (* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) DOC_GRAMMAR +Constr.ident: [ +| Prim.ident +] + +Prim.name: [ +| "_" +] + +global: [ +| Prim.reference +] + +constr_pattern: [ +| constr +] + +cpattern: [ +| lconstr +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" LIST1 universe_expr SEP "," ")" +| universe_expr +] + +lconstr: [ +| term200 +] + +constr: [ +| term8 +| "@" global univ_annot +] + +term200: [ +| binder_constr +| term100 +] + +term100: [ +| term99 "<:" term200 +| term99 "<<:" term200 +| term99 ":" term200 +| term99 ":>" +| term99 +] + +term99: [ +| term90 +] + +term90: [ +| term10 +] + +term10: [ +| term9 LIST1 arg +| "@" global univ_annot LIST0 term9 +| "@" pattern_ident LIST1 identref +| term9 +] + +term9: [ +| ".." term0 ".." +| term8 +] + +term8: [ +| term1 +] + +term1: [ +| term0 ".(" global LIST0 arg ")" +| term0 ".(" "@" global LIST0 ( term9 ) ")" +| term0 "%" IDENT +| term0 +] + +term0: [ +| atomic_constr +| term_match +| "(" term200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" term200 "}" +| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot +| "`(" term200 ")" +| "ltac" ":" "(" Pltac.ltac_expr ")" +] + +array_elems: [ +| LIST0 lconstr SEP ";" +] + +record_declaration: [ +| fields_def +] + +fields_def: [ +| field_def ";" fields_def +| field_def +| +] + +field_def: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," term200 +| "fun" open_binders "=>" term200 +| "let" name binders let_type_cstr ":=" term200 "in" term200 +| "let" "fix" fix_decl "in" term200 +| "let" "cofix" cofix_body "in" term200 +| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 case_type "in" term200 +| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 +| "if" term200 as_return_type "then" term200 "else" term200 +| "fix" fix_decls +| "cofix" cofix_decls +| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) +| "if" term200 "isn't" ssr_dthen ssr_else (* SSR plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* SSR plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) +] + +arg: [ +| test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| term9 +] + +atomic_constr: [ +| global univ_annot +| sort +| NUMBER +| string +| "_" +| "?" "[" identref "]" +| "?" "[" pattern_ident "]" +| pattern_ident evar_instance +] + +inst: [ +| identref ":=" lconstr +] + +evar_instance: [ +| "@{" LIST1 inst SEP ";" "}" +| +] + +univ_annot: [ +| "@{" LIST0 universe_level "}" +| +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_decls: [ +| fix_decl +| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref +] + +cofix_decls: [ +| cofix_body +| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref +] + +fix_decl: [ +| identref binders_fixannot type_cstr ":=" term200 +] + +cofix_body: [ +| identref binders type_cstr ":=" term200 +] + +term_match: [ +| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" +] + +case_item: [ +| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] +] + +case_type: [ +| "return" term100 +] + +as_return_type: [ +| OPT [ OPT [ "as" name ] case_type ] +] + +branches: [ +| OPT "|" LIST0 eqn SEP "|" +] + +mult_pattern: [ +| LIST1 pattern200 SEP "," +] + +eqn: [ +| LIST1 mult_pattern SEP "|" "=>" lconstr +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern +| +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" term200 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 LIST1 pattern1 +| "@" Prim.reference LIST0 pattern1 +| pattern1 +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| Prim.reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" +| NUMBER +| string +] + +fixannot: [ +| "{" "struct" identref "}" +| "{" "wf" constr identref "}" +| "{" "measure" constr OPT identref OPT constr "}" +] + +binders_fixannot: [ +| ensure_fixannot fixannot +| binder binders_fixannot +| +] + +open_binders: [ +| name LIST0 name ":" lconstr +| name LIST0 name binders +| name ".." name +| closed_binder binders +] + +binders: [ +| LIST0 binder +| Pcoq.Constr.binders +] + +binder: [ +| name +| closed_binder +] + +closed_binder: [ +| "(" name LIST1 name ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name LIST1 name ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name LIST1 name "}" +| "[" name "]" +| "[" name LIST1 name ":" lconstr "]" +| "[" name ":" lconstr "]" +| "[" name LIST1 name "]" +| "`(" LIST1 typeclass_constraint SEP "," ")" +| "`{" LIST1 typeclass_constraint SEP "," "}" +| "`[" LIST1 typeclass_constraint SEP "," "]" +| "'" pattern0 +| [ "of" | "&" ] term99 (* SSR plugin *) +] + +one_open_binder: [ +| name +| name ":" lconstr +| one_closed_binder +] + +one_closed_binder: [ +| "(" name ":" lconstr ")" +| "{" name "}" +| "{" name ":" lconstr "}" +| "[" name "]" +| "[" name ":" lconstr "]" +| "'" pattern0 +] + +typeclass_constraint: [ +| "!" term200 +| "{" name "}" ":" [ "!" | ] term200 +| test_name_colon name ":" [ "!" | ] term200 +| term200 +] + +type_cstr: [ +| ":" lconstr +| +] + +let_type_cstr: [ +| OPT [ ":" lconstr ] +] + +preident: [ +| IDENT +] + +ident: [ +| IDENT +] + +pattern_ident: [ +| LEFTQMARK ident +] + +identref: [ +| ident +] + +hyp: [ +| identref +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +qualid: [ +| reference +] + +by_notation: [ +| ne_string OPT [ "%" IDENT ] +] + +smart_global: [ +| reference +| by_notation +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident LIST0 field +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| bigint +] + +natural: [ +| bignat +] + +bigint: [ +| bignat +| test_minus_nat "-" bignat +] + +bignat: [ +| NUMBER +] + +bar_cbrace: [ +| test_pipe_closedcurly "|" "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "BackTo" natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| "Show" "Proof" "Diffs" OPT "removed" "." +| Pvernac.Vernac_.main_entry +] + opt_hintbases: [ | | ":" LIST1 IDENT @@ -981,492 +1467,6 @@ binder_interp: [ | "as" "strict" "pattern" ] -vernac_toplevel: [ -| "Drop" "." -| "Quit" "." -| "BackTo" natural "." -| test_show_goal "Show" "Goal" natural "at" natural "." -| "Show" "Proof" "Diffs" OPT "removed" "." -| Pvernac.Vernac_.main_entry -] - -Constr.ident: [ -| Prim.ident -] - -Prim.name: [ -| "_" -] - -global: [ -| Prim.reference -] - -constr_pattern: [ -| constr -] - -cpattern: [ -| lconstr -] - -sort: [ -| "Set" -| "Prop" -| "SProp" -| "Type" -| "Type" "@{" "_" "}" -| "Type" "@{" universe "}" -] - -sort_family: [ -| "Set" -| "Prop" -| "SProp" -| "Type" -] - -universe_increment: [ -| "+" natural -| -] - -universe_name: [ -| global -| "Set" -| "Prop" -] - -universe_expr: [ -| universe_name universe_increment -] - -universe: [ -| "max" "(" LIST1 universe_expr SEP "," ")" -| universe_expr -] - -lconstr: [ -| term200 -] - -constr: [ -| term8 -| "@" global univ_annot -] - -term200: [ -| binder_constr -| term100 -] - -term100: [ -| term99 "<:" term200 -| term99 "<<:" term200 -| term99 ":" term200 -| term99 ":>" -| term99 -] - -term99: [ -| term90 -] - -term90: [ -| term10 -] - -term10: [ -| term9 LIST1 arg -| "@" global univ_annot LIST0 term9 -| "@" pattern_ident LIST1 identref -| term9 -] - -term9: [ -| ".." term0 ".." -| term8 -] - -term8: [ -| term1 -] - -term1: [ -| term0 ".(" global LIST0 arg ")" -| term0 ".(" "@" global LIST0 ( term9 ) ")" -| term0 "%" IDENT -| term0 -] - -term0: [ -| atomic_constr -| term_match -| "(" term200 ")" -| "{|" record_declaration bar_cbrace -| "{" binder_constr "}" -| "`{" term200 "}" -| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot -| "`(" term200 ")" -| "ltac" ":" "(" Pltac.ltac_expr ")" -] - -array_elems: [ -| LIST0 lconstr SEP ";" -] - -record_declaration: [ -| fields_def -] - -fields_def: [ -| field_def ";" fields_def -| field_def -| -] - -field_def: [ -| global binders ":=" lconstr -] - -binder_constr: [ -| "forall" open_binders "," term200 -| "fun" open_binders "=>" term200 -| "let" name binders let_type_cstr ":=" term200 "in" term200 -| "let" "fix" fix_decl "in" term200 -| "let" "cofix" cofix_body "in" term200 -| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 -| "let" "'" pattern200 ":=" term200 "in" term200 -| "let" "'" pattern200 ":=" term200 case_type "in" term200 -| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 -| "if" term200 as_return_type "then" term200 "else" term200 -| "fix" fix_decls -| "cofix" cofix_decls -| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) -| "if" term200 "isn't" ssr_dthen ssr_else (* SSR plugin *) -| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* SSR plugin *) -| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) -| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) -] - -arg: [ -| test_lpar_id_coloneq "(" identref ":=" lconstr ")" -| term9 -] - -atomic_constr: [ -| global univ_annot -| sort -| NUMBER -| string -| "_" -| "?" "[" identref "]" -| "?" "[" pattern_ident "]" -| pattern_ident evar_instance -] - -inst: [ -| identref ":=" lconstr -] - -evar_instance: [ -| "@{" LIST1 inst SEP ";" "}" -| -] - -univ_annot: [ -| "@{" LIST0 universe_level "}" -| -] - -universe_level: [ -| "Set" -| "Prop" -| "Type" -| "_" -| global -] - -fix_decls: [ -| fix_decl -| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref -] - -cofix_decls: [ -| cofix_body -| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref -] - -fix_decl: [ -| identref binders_fixannot type_cstr ":=" term200 -] - -cofix_body: [ -| identref binders type_cstr ":=" term200 -] - -term_match: [ -| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" -] - -case_item: [ -| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] -] - -case_type: [ -| "return" term100 -] - -as_return_type: [ -| OPT [ OPT [ "as" name ] case_type ] -] - -branches: [ -| OPT "|" LIST0 eqn SEP "|" -] - -mult_pattern: [ -| LIST1 pattern200 SEP "," -] - -eqn: [ -| LIST1 mult_pattern SEP "|" "=>" lconstr -] - -record_pattern: [ -| global ":=" pattern200 -] - -record_patterns: [ -| record_pattern ";" record_patterns -| record_pattern -| -] - -pattern200: [ -| pattern100 -] - -pattern100: [ -| pattern99 ":" term200 -| pattern99 -] - -pattern99: [ -| pattern90 -] - -pattern90: [ -| pattern10 -] - -pattern10: [ -| pattern1 "as" name -| pattern1 LIST1 pattern1 -| "@" Prim.reference LIST0 pattern1 -| pattern1 -] - -pattern1: [ -| pattern0 "%" IDENT -| pattern0 -] - -pattern0: [ -| Prim.reference -| "{|" record_patterns bar_cbrace -| "_" -| "(" pattern200 ")" -| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" -| NUMBER -| string -] - -fixannot: [ -| "{" "struct" identref "}" -| "{" "wf" constr identref "}" -| "{" "measure" constr OPT identref OPT constr "}" -] - -binders_fixannot: [ -| ensure_fixannot fixannot -| binder binders_fixannot -| -] - -open_binders: [ -| name LIST0 name ":" lconstr -| name LIST0 name binders -| name ".." name -| closed_binder binders -] - -binders: [ -| LIST0 binder -| Pcoq.Constr.binders -] - -binder: [ -| name -| closed_binder -] - -closed_binder: [ -| "(" name LIST1 name ":" lconstr ")" -| "(" name ":" lconstr ")" -| "(" name ":=" lconstr ")" -| "(" name ":" lconstr ":=" lconstr ")" -| "{" name "}" -| "{" name LIST1 name ":" lconstr "}" -| "{" name ":" lconstr "}" -| "{" name LIST1 name "}" -| "[" name "]" -| "[" name LIST1 name ":" lconstr "]" -| "[" name ":" lconstr "]" -| "[" name LIST1 name "]" -| "`(" LIST1 typeclass_constraint SEP "," ")" -| "`{" LIST1 typeclass_constraint SEP "," "}" -| "`[" LIST1 typeclass_constraint SEP "," "]" -| "'" pattern0 -| [ "of" | "&" ] term99 (* SSR plugin *) -] - -one_open_binder: [ -| name -| name ":" lconstr -| one_closed_binder -] - -one_closed_binder: [ -| "(" name ":" lconstr ")" -| "{" name "}" -| "{" name ":" lconstr "}" -| "[" name "]" -| "[" name ":" lconstr "]" -| "'" pattern0 -] - -typeclass_constraint: [ -| "!" term200 -| "{" name "}" ":" [ "!" | ] term200 -| test_name_colon name ":" [ "!" | ] term200 -| term200 -] - -type_cstr: [ -| ":" lconstr -| -] - -let_type_cstr: [ -| OPT [ ":" lconstr ] -] - -preident: [ -| IDENT -] - -ident: [ -| IDENT -] - -pattern_ident: [ -| LEFTQMARK ident -] - -identref: [ -| ident -] - -hyp: [ -| identref -] - -field: [ -| FIELD -] - -fields: [ -| field fields -| field -] - -fullyqualid: [ -| ident fields -| ident -] - -name: [ -| "_" -| ident -] - -reference: [ -| ident fields -| ident -] - -qualid: [ -| reference -] - -by_notation: [ -| ne_string OPT [ "%" IDENT ] -] - -smart_global: [ -| reference -| by_notation -] - -ne_string: [ -| STRING -] - -ne_lstring: [ -| ne_string -] - -dirpath: [ -| ident LIST0 field -] - -string: [ -| STRING -] - -lstring: [ -| string -] - -integer: [ -| bigint -] - -natural: [ -| bignat -] - -bigint: [ -| bignat -| test_minus_nat "-" bignat -] - -bignat: [ -| NUMBER -] - -bar_cbrace: [ -| test_pipe_closedcurly "|" "}" -] - -strategy_level: [ -| "expand" -| "opaque" -| integer -| "transparent" -] - simple_tactic: [ | "btauto" | "congruence" @@ -1778,7 +1778,6 @@ simple_tactic: [ | "zify_iter_let" tactic (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string "in" ident (* ring plugin *) | "protect_fv" string (* ring plugin *) | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) @@ -3283,7 +3282,7 @@ ltac2_expr6: [ ] ltac2_expr5: [ -| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6 (* Ltac2 plugin *) +| "fun" LIST1 G_LTAC2_input_fun type_cast "=>" ltac2_expr6 (* Ltac2 plugin *) | "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) | "match" ltac2_expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *) | "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) @@ -3371,8 +3370,13 @@ tac2expr_in_env: [ | ltac2_expr6 (* Ltac2 plugin *) ] +type_cast: [ +| (* Ltac2 plugin *) +| ":" ltac2_type5 (* Ltac2 plugin *) +] + G_LTAC2_let_clause: [ -| let_binder ":=" ltac2_expr6 (* Ltac2 plugin *) +| let_binder type_cast ":=" ltac2_expr6 (* Ltac2 plugin *) ] let_binder: [ @@ -3415,7 +3419,7 @@ G_LTAC2_input_fun: [ ] tac2def_body: [ -| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6 (* Ltac2 plugin *) +| G_LTAC2_binder LIST0 G_LTAC2_input_fun type_cast ":=" ltac2_expr6 (* Ltac2 plugin *) ] tac2def_val: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5674d28139..40bb980e90 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1856,7 +1856,6 @@ simple_tactic: [ | "zify_iter_let" ltac_expr (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" one_term (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string OPT ( "in" ident ) | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) @@ -2274,7 +2273,7 @@ ltac2_entry: [ ] tac2def_body: [ -| [ "_" | ident ] LIST0 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *) +| [ "_" | ident ] LIST0 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr (* Ltac2 plugin *) ] tac2typ_def: [ @@ -2315,13 +2314,13 @@ ltac2_expr: [ ] ltac2_expr5: [ -| "fun" LIST1 tac2pat0 "=>" ltac2_expr (* Ltac2 plugin *) +| "fun" LIST1 tac2pat0 OPT ( ":" ltac2_type ) "=>" ltac2_expr (* Ltac2 plugin *) | "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr (* Ltac2 plugin *) | ltac2_expr3 (* Ltac2 plugin *) ] ltac2_let_clause: [ -| LIST1 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *) +| LIST1 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr (* Ltac2 plugin *) ] ltac2_expr3: [ |