diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 31 | ||||
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/language/core/modules.rst | 72 | ||||
| -rw-r--r-- | doc/sphinx/language/core/primitive.rst | 17 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 44 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 88 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/logic.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 76 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 29 |
13 files changed, 230 insertions, 178 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 3bd85d29c8..5d471c695c 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -31,9 +31,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, .. flag:: Simplex + .. deprecated:: 8.14 + This flag (set by default) instructs the decision procedures to - use the Simplex method for solving linear goals. If it is not set, - the decision procedures are using Fourier elimination. + use the Simplex method for solving linear goals instead of the + deprecated Fourier elimination. .. opt:: Dump Arith diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 2b24ced8a1..8f2b51ccce 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -320,14 +320,6 @@ optional tactic is replaced by the default one if not specified. (the default), or if the system should infer which obligations can be declared opaque. -.. flag:: Hide Obligations - - .. deprecated:: 8.12 - - Controls whether obligations appearing in the - term should be hidden as implicit arguments of the special - constant ``Program.Tactics.obligation``. - The module :g:`Coq.Program.Tactics` defines the default tactic for solving obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also adds some useful notations, as documented in the file itself. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 7db54987d6..8fa1b97851 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -82,13 +82,13 @@ Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann. -The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric +The 51 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, Cyril Cohen, Julien Coolen, Matthew Dempsky, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesús Gallego Arias, Paolo G. Giarrusso, Attila Gáspár, Gaëtan Gilbert, Jason Gross, Benjamin Grégoire, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Ignat Insarov, Ralf Jung, Fabian Kunze, Vincent Laporte, Olivier Laurent, Larry D. Lee Jr, -Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet, +Thomas Letan, Yishuai Li, James Lottes, Jean-Christophe Léchenet, Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond, Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau, @@ -701,6 +701,27 @@ Commands and options (`#13556 <https://github.com/coq/coq/pull/13556>`_, by Simon Friis Vindum). +Changes in 8.13.1 +~~~~~~~~~~~~~~~~~ + +Kernel +^^^^^^ + +- **Fixed:** + Fix arities of VM opcodes for some floating-point operations + that could cause memory corruption + (`#13867 <https://github.com/coq/coq/pull/13867>`_, + by Guillaume Melquiond). + +CoqIDE +^^^^^^ + +- **Added:** + Option ``-v`` and ``--version`` to CoqIDE + (`#13870 <https://github.com/coq/coq/pull/13870>`_, + by Guillaume Melquiond). + + Version 8.12 ------------ @@ -1230,7 +1251,7 @@ Flags, options and attributes :attr:`universes(template)` and ``universes(notemplate)`` instead (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). - **Deprecated:** - :flag:`Hide Obligations` flag + `Hide Obligations` flag (`#11828 <https://github.com/coq/coq/pull/11828>`_, by Emilio Jesus Gallego Arias). - **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical @@ -1301,7 +1322,7 @@ Commands Declaration of arbitrary terms as hints. Global references are now preferred (`#7791 <https://github.com/coq/coq/pull/7791>`_, by Pierre-Marie Pédrot). -- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:` +- **Deprecated:** `SearchHead` in favor of the new `headconcl:` clause of :cmd:`Search` (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann). - **Added:** @@ -3191,7 +3212,7 @@ Other changes in 8.10+beta1 by Maxime Dénès, review by Pierre-Marie Pédrot). - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a - documented replacement of :tacn:`convert_concl_no_check` + documented replacement of `convert_concl_no_check` (`#10012 <https://github.com/coq/coq/pull/10012>`_, `#10017 <https://github.com/coq/coq/pull/10017>`_, `#10053 <https://github.com/coq/coq/pull/10053>`_, and diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 8dbc1626ba..7566996ef6 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -9,7 +9,7 @@ Binders .. insertprodn open_binders binder .. prodn:: - open_binders ::= {+ @name } : @term + open_binders ::= {+ @name } : @type | {+ @binder } name ::= _ | @ident diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 0a61c4ce22..2b50d4c420 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -523,31 +523,20 @@ they appear after a boldface label. They are listed in the Locality attributes supported by :cmd:`Set` and :cmd:`Unset` ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, -:attr:`global` and :attr:`export` locality attributes: - -* no attribute: the original setting is *not* restored at the end of - the current module or section. -* :attr:`local` (or alternatively, the ``Local`` prefix): the setting - is applied within the current module or section. The original value - of the setting is restored at the end of the current module or - section. -* :attr:`export` (or alternatively, the ``Export`` prefix): similar to - :attr:`local`, the original value of the setting is restored at the - end of the current module or section. In addition, if the value is - set in a module, then :cmd:`Import`\-ing the module sets the option - or flag. -* :attr:`global` (or alternatively, the ``Global`` prefix): the - original setting is *not* restored at the end of the current module - or section. In addition, if the value is set in a file, then - :cmd:`Require`\-ing the file sets the option. +The :cmd:`Set` and :cmd:`Unset` commands support the mutually +exclusive :attr:`local`, :attr:`export` and :attr:`global` locality +attributes (or the ``Local``, ``Export`` or ``Global`` prefixes). + +If no attribute is specified, the original value of the flag or option +is restored at the end of the current module but it is *not* restored +at the end of the current section. Newly opened modules and sections inherit the current settings. .. note:: - We discourage using the :attr:`global` attribute with the :cmd:`Set` and - :cmd:`Unset` commands. If your goal is to define + We discourage using the :attr:`global` locality attribute with the + :cmd:`Set` and :cmd:`Unset` commands. If your goal is to define project-wide settings, you should rather use the command-line arguments ``-set`` and ``-unset`` for setting flags and options (see :ref:`command-line-options`). diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 93d70c773f..2e678c49d8 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -880,7 +880,7 @@ started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-opt .. _qualified-names: Qualified identifiers ---------------------- +~~~~~~~~~~~~~~~~~~~~~ .. insertprodn qualid field_ident @@ -1010,3 +1010,73 @@ subdirectories of path). See the command :cmd:`Declare ML Module` in See :ref:`command-line-options` for a more general view over the Coq command line options. + +.. _controlling-locality-of-commands: + +Controlling the scope of commands with locality attributes +---------------------------------------------------------- + +Many commands have effects that apply only within a specific scope, +typically the section or the module in which the command was +called. Locality :term:`attributes <attribute>` can alter the scope of +the effect. Below, we give the semantics of each locality attribute +while noting a few exceptional commands for which :attr:`local` and +:attr:`global` attributes are interpreted differently. + +.. attr:: local + + The :attr:`local` attribute limits the effect of the command to the + current scope (section or module). + + The ``Local`` prefix is an alternative syntax for the :attr:`local` + attribute (see :n:`@legacy_attr`). + + .. note:: + + - For some commands, this is the only locality supported within + sections (e.g., for :cmd:`Notation`, :cmd:`Ltac` and + :ref:`Hint <creating_hints>` commands). + + - For some commands, this is the default locality within + sections even though other locality attributes are supported + as well (e.g., for the :cmd:`Arguments` command). + + .. warning:: + + **Exception:** when :attr:`local` is applied to + :cmd:`Definition`, :cmd:`Theorem` or their variants, its + semantics are different: it makes the defined objects available + only through their fully-qualified names rather than their + unqualified names after an :cmd:`Import`. + +.. attr:: export + + The :attr:`export` attribute makes the effect of the command + persist when the section is closed and applies the effect when the + module containing the command is imported. + + Commands supporting this attribute include :cmd:`Set`, :cmd:`Unset` + and the :ref:`Hint <creating_hints>` commands, although the latter + don't support it within sections. + +.. attr:: global + + The :attr:`global` attribute makes the effect of the command + persist even when the current section or module is closed. Loading + the file containing the command (possibly transitively) applies the + effect of the command. + + The ``Global`` prefix is an alternative syntax for the + :attr:`global` attribute (see :n:`@legacy_attr`). + + .. warning:: + + **Exception:** for a few commands (like :cmd:`Notation` and + :cmd:`Ltac`), this attribute behaves like :attr:`export`. + + .. warning:: + + We strongly discourage using the :attr:`global` locality + attribute because the transitive nature of file loading gives + the user little control. We recommend using the :attr:`export` + locality attribute where it is supported. diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index 4505fc4b4d..7211d00dd0 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -8,15 +8,20 @@ Primitive Integers The language of terms features 63-bit machine integers as values. The type of such a value is *axiomatized*; it is declared through the following sentence -(excerpt from the :g:`Int63` module): +(excerpt from the :g:`PrimInt63` module): .. coqdoc:: Primitive int := #int63_type. -This type is equipped with a few operators, that must be similarly declared. -For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, -declared and specified as follows: +This type can be understood as representing either unsigned or signed integers, +depending on which module is imported or, more generally, which scope is open. +:g:`Int63` and :g:`int63_scope` refer to the unsigned version, while :g:`Sint63` +and :g:`sint63_scope` refer to the signed one. + +The :g:`PrimInt63` module declares the available operators for this type. +For instance, equality of two unsigned primitive integers can be determined using +the :g:`Int63.eqb` function, declared and specified as follows: .. coqdoc:: @@ -25,7 +30,9 @@ declared and specified as follows: Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. -The complete set of such operators can be obtained looking at the :g:`Int63` module. +The complete set of such operators can be found in the :g:`PrimInt63` module. +The specifications and notations are in the :g:`Int63` and :g:`Sint63` +modules. These primitive declarations are regular axioms. As such, they must be trusted and are listed by the :g:`Print Assumptions` command, as in the following example. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index dcc60195ed..e7237cf7eb 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -248,7 +248,7 @@ right arrow, or ``\>=`` for a greater than or equal sign. A larger number of latex tokens are supported by default. The full list is available here: -https://github.com/coq/coq/blob/master/ide/default_bindings_src.ml +https://github.com/coq/coq/blob/master/ide/coqide/default_bindings_src.ml Custom bindings may be added, as explained further on. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 766f7ab44e..071fcbee11 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -77,7 +77,7 @@ specified, the default selector is used. .. todo: fully describe selectors. At the moment, ltac has a fairly complete description .. todo: mention selectors can be applied to some commands, such as - Check, Search, SearchHead, SearchPattern, SearchRewrite. + Check, Search, SearchPattern, SearchRewrite. .. opt:: Default Goal Selector "@toplevel_selector" :name: Default Goal Selector @@ -498,10 +498,16 @@ one or more of its hypotheses. :n:`{? - } {+ @nat_or_var }` Selects the specified occurrences within a single goal or hypothesis. - Occurrences are numbered from left to right starting with 1 when the - goal is printed with the :flag:`Printing All` flag. (In particular, occurrences - in :ref:`implicit arguments <ImplicitArguments>` and - :ref:`coercions <Coercions>` are counted but not shown by default.) + Occurrences are numbered starting with 1 following a depth-first traversal + of the term's expression, including occurrences in + :ref:`implicit arguments <ImplicitArguments>` + and :ref:`coercions <Coercions>` that are not displayed by default. + (Set the :flag:`Printing All` flag to show those in the printed term.) + + For example, when matching the pattern `_ + _` in the term `(a + b) + c`, + occurrence 1 is `(...) + c` and + occurrence 2 is `(a + b)`. When matching that pattern with term `a + (b + c)`, + occurrence 1 is `a + (...)` and occurrence 2 is `b + c`. Specifying `-` includes all occurrences *except* the ones listed. @@ -669,10 +675,10 @@ Applying theorems :tacn:`notypeclasses refine`: it performs type checking without resolution of typeclasses, does not perform beta reductions or shelve the subgoals. - .. flag:: Debug Unification - - Enables printing traces of unification steps used during - elaboration/typechecking and the :tacn:`refine` tactic. + :opt:`Debug` ``"unification"`` enables printing traces of + unification steps used during elaboration/typechecking and the + :tacn:`refine` tactic. ``"ho-unification"`` prints information + about higher order heuristics. .. tacn:: apply @term :name: apply @@ -1034,10 +1040,9 @@ Applying theorems when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). -.. flag:: Debug Tactic Unification - - Enables printing traces of unification steps in tactic unification. - Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. +:opt:`Debug` ``"tactic-unification"`` enables printing traces of +unification steps in tactic unification. Tactic unification is used in +tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: @@ -2067,19 +2072,6 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent premise of the goal. -.. tacn:: double induction @ident @ident - :name: double induction - - This tactic is deprecated and should be replaced by - :n:`induction @ident; induction @ident` (or - :n:`induction @ident ; destruct @ident` depending on the exact needs). - -.. tacv:: double induction @natural__1 @natural__2 - - This tactic is deprecated and should be replaced by - :n:`induction num1; induction num3` where :n:`num3` is the result - of :n:`num2 - num1` - .. tacn:: dependent induction @ident :name: dependent induction diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 8e2f577f6b..37d605360d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -312,31 +312,6 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Search is:Instance [ Reflexive | Symmetric ]. -.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } } - - .. deprecated:: 8.12 - - Use the `headconcl:` clause of :cmd:`Search` instead. - - Displays the name and type of all hypotheses of the - selected goal (if any) and theorems of the current context that have the - form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern` - matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b` - matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`. - - See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - - .. example:: :cmd:`SearchHead` examples - - .. coqtop:: none reset - - Add Search Blacklist "internal_". - - .. coqtop:: all warn - - SearchHead le. - SearchHead (@eq bool). - .. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the @@ -384,7 +359,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. table:: Search Blacklist @string Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, - :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose + :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose fully-qualified name contains any of the strings will be excluded from the search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and ``Private_``. @@ -395,7 +370,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. flag:: Search Output Name Only This flag restricts the output of search commands to identifier names; - turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, + turning it on causes invocations of :cmd:`Search`, :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their output, printing only identifiers. @@ -890,6 +865,14 @@ Controlling display interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that `A,-A` is equivalent to `-A`. +.. opt:: Debug "{+, {? - } @ident }" + + Configures the display of debug messages. Each :n:`@ident` enables debug messages + for that component, while :n:`-@ident` disables messages for the component. + ``all`` activates or deactivates all other components. ``backtrace`` controls printing of + error backtraces. + + :cmd:`Test` `Debug` displays the list of components and their enabled/disabled state. .. opt:: Printing Width @natural This command sets which left-aligned part of the width of the screen is used @@ -1083,57 +1066,6 @@ described first. .. seealso:: :ref:`performingcomputations` -.. _controlling-locality-of-commands: - -Controlling the locality of commands ------------------------------------------ - -.. attr:: global - local - - Some commands support a :attr:`local` or :attr:`global` attribute - to control the scope of their effect. There is also a legacy (and - much more commonly used) syntax using the ``Local`` or ``Global`` - prefixes (see :n:`@legacy_attr`). There are four kinds of - commands: - - + Commands whose default is to extend their effect both outside the - section and the module or library file they occur in. For these - commands, the :attr:`local` attribute limits the effect of the command to the - current section or module it occurs in. As an example, the :cmd:`Coercion` - and :cmd:`Strategy` commands belong to this category. - + Commands whose default behavior is to stop their effect at the end - of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the :attr:`local` attribute limits the - effect of the command to the current module if the command does not occur in a - section and the :attr:`global` attribute extends the effect outside the current - sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong - to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the :attr:`global` attribute is not - applicable to them. - + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the :attr:`global` - attribute extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` commands - belong to this category. - + Commands whose default behavior is to extend their effect outside - sections but not outside modules when they occur in a section and to - extend their effect outside the module or library file they occur in - when no section contains them. For these commands, the :attr:`local` attribute - limits the effect to the current section or module while the :attr:`global` - attribute extends the effect outside the module even when the command - occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this - category. - -.. attr:: export - - Some commands support an :attr:`export` attribute. The effect of - the attribute is to make the effect of the command available when - the module containing it is imported. It is supported in - particular by the :ref:`Hint <creating_hints>`, :cmd:`Set` and :cmd:`Unset` - commands. - .. _controlling-typing-flags: Controlling Typing Flags diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index 5aaded2726..3f1f5d46c5 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -194,9 +194,7 @@ Solvers for logic and equality additional arguments can be given to congruence by filling in the holes in the terms given in the error message, using the `with` clause. - .. flag:: Congruence Verbose - - Makes :tacn:`congruence` print debug information. + :opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information. .. tacn:: btauto diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 8c8c88c526..4f937ad727 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -44,11 +44,14 @@ Rewriting with Leibniz and setoid equality oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings one_term_with_bindings ::= {? > } @one_term {? with @bindings } - Rewrites terms based on equalities. The type of :n:`@one_term` must have the form: + Replaces subterms with other subterms that have been proven to be equal. + The type of :n:`@one_term` must have the form: :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2` - where :g:`EQ` is the Leibniz equality `eq` or a registered setoid equality. + .. todo :term:`Leibniz equality` does not work with Sphinx 2.3.1. It does with Sphinx 3.0.3. + + where :g:`EQ` is the Leibniz equality `eq` or a registered :term:`setoid equality`. Note that :n:`eq @term__1 @term__2` is typically written with the infix notation :n:`@term__1 = @term__2`. You must `Require Setoid` to use the tactic with a setoid equality or with :ref:`setoid rewriting <generalizedrewriting>`. @@ -61,7 +64,7 @@ Rewriting with Leibniz and setoid equality Some of the variables :g:`x`\ :sub:`i` are solved by unification, and some of the types :n:`A__1, ..., A__n` may become new subgoals. :tacn:`rewrite` won't find occurrences inside `forall` that refer - to variables bound by the `forall`; use :tacn:`setoid_rewrite` + to variables bound by the `forall`; use the more advanced :tacn:`setoid_rewrite` if you want to find such occurrences. :n:`{+, @oriented_rewriter }` @@ -90,12 +93,55 @@ Rewriting with Leibniz and setoid equality any of them can be rewritten. If not specified, only the first occurrence in the conclusion is replaced. - If :n:`at @occs_nums` is specified, rewriting is always done with - :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality. + .. note:: + + If :n:`at @occs_nums` is specified, rewriting is always done + with :ref:`setoid rewriting <generalizedrewriting>`, even for + Leibniz equality, which means that you must `Require + Setoid` to use that form. However, note that :tacn:`rewrite` + (even when using setoid rewriting) and :tacn:`setoid_rewrite` + don't behave identically (as is noted above and below). :n:`by @ltac_expr3` If specified, is used to resolve all side conditions generated by the tactic. + .. note:: + + For each selected hypothesis and/or the conclusion, + :tacn:`rewrite` finds the first matching subterm in + depth-first search order. Only subterms identical to + that first matched subterm are rewritten. If the `at` clause is specified, + only these subterms are considered when counting occurrences. + To select a different set of matching subterms, you can + specify how some or all of the free variables are bound by + using a `with` clause (see :n:`@one_term_with_bindings`). + + For instance, if we want to rewrite the right-hand side in the + following goal, this will not work: + + .. coqtop:: none + + Require Import Arith. + + .. coqtop:: out + + Lemma example x y : x + y = y + x. + + .. coqtop:: all fail + + rewrite Nat.add_comm at 2. + + One can explicitly specify how some variables are bound to match + a different subterm: + + .. coqtop:: all abort + + rewrite Nat.add_comm with (m := x). + + Note that the more advanced :tacn:`setoid_rewrite` tactic + behaves differently, and thus the number of occurrences + available to rewrite may differ between the two tactics. + .. exn:: Tactic failure: Setoid library not loaded. :undocumented: @@ -338,13 +384,6 @@ Rewriting with definitional equality exact H. Qed. - .. tacn:: convert_concl_no_check @one_term - - .. deprecated:: 8.11 - - Deprecated old name for :tacn:`change_no_check`. Does not support any of its - variants. - .. _performingcomputations: Performing computations @@ -520,9 +559,7 @@ the conversion in hypotheses :n:`{+ @ident}`. on the profile file to see the results. Consult the ``perf`` documentation for more details. -.. flag:: Debug Cbv - - This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print + :opt:`Debug` ``"Cbv"`` makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it makes. @@ -538,9 +575,6 @@ the conversion in hypotheses :n:`{+ @ident}`. definition (say :g:`t`) and then reduces :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. -.. exn:: Not reducible. - :undocumented: - .. exn:: No head constant to reduce. :undocumented: @@ -623,10 +657,8 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). -.. flag:: Debug RAKAM - - This flag makes :tacn:`cbn` print various debugging information. - ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. +:opt:`Debug` ``"RAKAM"`` makes :tacn:`cbn` print various debugging information. +``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. .. tacn:: unfold @qualid :name: unfold diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 609884ce1d..557ef10555 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1726,12 +1726,6 @@ Number notations * :n:`@qualid__type -> Number.number` * :n:`@qualid__type -> option Number.number` - .. deprecated:: 8.12 - Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and - :g:`Decimal.decimal` are replaced respectively by number - notations on :g:`Number.uint`, :g:`Number.int` and - :g:`Number.number`. - When parsing, the application of the parsing function :n:`@qualid__parse` to the number will be fully reduced, and universes of the resulting term will be refreshed. @@ -1741,6 +1735,12 @@ Number notations sorts, primitive integers, primitive floats, primitive arrays and type constants for primitive types) will be considered for printing. + .. note:: + For example, :n:`@qualid__type` can be :n:`PrimInt63.int`, + in which case :n:`@qualid__print` takes :n:`PrimInt63.int_wrapper` as input + instead of :n:`PrimInt63.int`. See below for an + :ref:`example <example-number-notation-primitive-int>`. + .. _number-string-via: :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` @@ -2066,6 +2066,23 @@ The following errors apply to both string and number notations: Check 3. +.. _example-number-notation-primitive-int: + +.. example:: Number Notation for primitive integers + + This shows the use of the primitive + integers :n:`PrimInt63.int` as :n:`@qualid__type`. It is the way + parsing and printing of primitive integers are actually implemented + in `PrimInt63.v`. + + .. coqtop:: in reset + + Require Import Int63. + Definition parser (x : pos_neg_int63) : option int := + match x with Pos p => Some p | Neg _ => None end. + Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). + Number Notation int parser printer : int63_scope. + .. _example-number-notation-non-inductive: .. example:: Number Notation for a non inductive type |