diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 20 |
5 files changed, 9 insertions, 57 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 395b5ce2d3..7e698bfb66 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -144,6 +144,8 @@ Many other commands support the ``Polymorphic`` flag, including: - ``Lemma``, ``Axiom``, and all the other “definition” keywords support polymorphism. +- :cmd:`Section` will locally set the polymorphism flag inside the section. + - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support polymorphism. This means that the universe variables (and associated constraints) are discharged polymorphically over definitions that use diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index fd84868a1f..6ac55e7bf4 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -102,10 +102,10 @@ reference manual. Here are the most important user-visible changes: extensionality lemma: - interactive mode: :n:`under @term`, associated terminator: :tacn:`over` - - one-liner mode: `under @term do [@tactic | ...]` + - one-liner mode: :n:`under @term do [@tactic | ...]` It can take occurrence switches, contextual patterns, and intro patterns: - :g:`under {2}[in RHS]eq_big => [i|i ?] do ...` + :g:`under {2}[in RHS]eq_big => [i|i ?]` (`#9651 <https://github.com/coq/coq/pull/9651>`_, by Erik Martin-Dorel and Enrico Tassi). diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index efb5df720a..7d6171285e 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -88,8 +88,6 @@ There are other buttons on the |CoqIDE| toolbar: a button to save the running buffer; a button to close the current buffer (an "X"); buttons to switch among buffers (left and right arrows); an "information" button; and a "gears" button. -The "information" button is described in Section :ref:`try-tactics-automatically`. - The "gears" button submits proof terms to the |Coq| kernel for type checking. When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. @@ -100,27 +98,6 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -.. _try-tactics-automatically: - -Trying tactics automatically ------------------------------- - -The menu Try Tactics provides some features for automatically trying -to solve the current goal using simple tactics. If such a tactic -succeeds in solving the goal, then its text is automatically inserted -into the script. There is finally a combination of these tactics, -called the *proof wizard* which will try each of them in turn. This -wizard is also available as a tool button (the "information" button). The set of -tactics tried by the wizard is customizable in the preferences. - -These tactics are general ones, in particular they do not refer to -particular hypotheses. You may also try specific tactics related to -the goal or one of the hypotheses, by clicking with the right mouse -button on the goal or the considered hypothesis. This is the -“contextual menu on goals” feature, that may be disabled in the -preferences if undesirable. - - Proof folding ------------------ @@ -202,13 +179,6 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -The `Tactics Wizard` section allows defining the set of tactics that -should be tried, in sequence, to solve the current goal. - -The last section is for miscellaneous boolean settings, such as the -“contextual menu on goals” feature presented in the section -:ref:`Try tactics automatically <try-tactics-automatically>`. - Notice that these settings are saved in the file `.coqiderc` of your home directory. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1b9e3ce0f3..ed980bd4de 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3761,10 +3761,10 @@ involves the following steps: 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. - These protected goals are displayed using the ``Under[ … ]`` - notation (e.g. ``Under[ m - m ]`` in the running example). + These protected goals are displayed using the ``'Under[ … ]`` + notation (e.g. ``'Under[ m - m ]`` in the running example). -6. The expression inside the ``Under[ … ]`` notation can be +6. The expression inside the ``'Under[ … ]`` notation can be proved equivalent to the desired expression by using a regular :tacn:`rewrite` tactic. @@ -3782,7 +3782,7 @@ The over tactic Two equivalent facilities (a terminator and a lemma) are provided to close intermediate subgoals generated by :tacn:`under` (i.e. goals -displayed as ``Under[ … ]``): +displayed as ``'Under[ … ]``): .. tacn:: over :name: over @@ -3792,7 +3792,7 @@ displayed as ``Under[ … ]``): .. tacv:: by rewrite over - This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. .. _under_one_liner: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5f3e82938d..774732825a 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -870,26 +870,6 @@ interactively, they cannot be part of a vernacular file loaded via have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. - .. cmdv:: Backtrack @num @num @num - :name: Backtrack - - .. deprecated:: 8.4 - - :cmd:`Backtrack` is a *deprecated* form of - :cmd:`BackTo` which allows explicitly manipulating the proof environment. The - three numbers represent the following: - - + *first number* : State label to reach, as for :cmd:`BackTo`. - + *second number* : *Proof state number* to unbury once aborts have been done. - |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`). - + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently - opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`). - - .. exn:: Invalid backtrack. - - The destination state label is unknown. - - .. _quitting-and-debugging: Quitting and debugging |