diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 63 |
4 files changed, 53 insertions, 20 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 1643baf0e8..2264b170fc 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -303,7 +303,7 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de it names the introduced hypothesis :token:`ident`. Note that this example also uses ``:token:``. That's because ``ident`` is - defined in the the Coq manual as a grammar production, and ``:token:`` + defined in the Coq manual as a grammar production, and ``:token:`` creates a link to that. When referring to a placeholder that happens to be a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 0f51b3eba3..4e42bddee2 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -90,8 +90,8 @@ not set, they look for the commands in the executable path. The ``$COQ_COLORS`` environment variable can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated -list of assignments of the form ``name=``:n:``{*; attr}`` where -``name`` is the name of the corresponding highlight tag and each ``attrᵢ`` is an +list of assignments of the form :n:`name={*; attr}` where +``name`` is the name of the corresponding highlight tag and each ``attr`` is an ANSI escape code. The list of highlight tags can be retrieved with the ``-list-tags`` command-line option of ``coqtop``. @@ -107,7 +107,7 @@ and ``coqtop``, unless stated otherwise: to the OCaml loadpath. See also: :ref:`names-of-libraries` and the command Declare ML Module Section :ref:`compiled-files`. :-Q *directory* dirpath: Add physical path *directory* to the list of - directories where |Coq| looks for a file and bind it to the the logical + directories where |Coq| looks for a file and bind it to the logical directory *dirpath*. The subdirectory structure of *directory* is recursively available from |Coq| using absolute names (extending the dirpath prefix) (see Section :ref:`qualified-names`).Note that only those diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 6fbb2fac6d..0310dbead5 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -391,7 +391,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics: focused goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails when there is no applicable tactic. In other words, - :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first + :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the first :n:`v__i` to have *at least* one success. .. exn:: No applicable tactic. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index a9d0c16376..b49d0f0504 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -329,20 +329,47 @@ Navigation in the proof tree .. cmdv:: @num: %{ - This focuses on the :token:`num` th subgoal to prove. + This focuses on the :token:`num`\-th subgoal to prove. - Error messages: + .. cmdv:: [@ident]: %{ + + This focuses on the named goal :token:`ident`. + + .. note:: + + Goals are just existential variables and existential variables do not + get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + + .. seealso:: :ref:`existential-variables` + + .. example:: + + This can also be a way of focusing on a shelved goal, for instance: + + .. coqtop:: all + + Goal exists n : nat, n = n. + eexists ?[x]. + reflexivity. + [x]: exact 0. + Qed. .. exn:: This proof is focused, but cannot be unfocused this way. You are trying to use ``}`` but the current subproof has not been fully solved. - .. exn:: No such goal. - :name: No such goal. (Focusing) + .. exn:: No such goal (@num). + :undocumented: + + .. exn:: No such goal (@ident). + :undocumented: - .. exn:: Brackets only support the single numbered goal selector. + .. exn:: Brackets do not support multi-goal selectors. - See also error messages about bullets below. + Brackets are used to focus on a single goal given either by its position + or by its name if it has one. + + .. seealso:: The error messages about bullets below. .. _bullets: @@ -358,8 +385,10 @@ same bullet ``b``. See the example below. Different bullets can be used to nest levels. The scope of bullet does not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further -nesting levels provided they are delimited by these. Available bullets -are ``-``, ``+``, ``*``, ``--``, ``++``, ``**``, ``---``, ``+++``, ``***``, ... (without a terminating period). +nesting levels provided they are delimited by these. Bullets are made of +repeated ``-``, ``+`` or ``*`` symbols: + +.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * } Note again that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or ``}`` to unfocus it @@ -392,19 +421,23 @@ The following example script illustrates all these features: - assert True. { trivial. } assumption. + Qed. +.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished. -.. exn:: Wrong bullet @bullet1: Current bullet @bullet2 is not finished. - - Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same. + Before using bullet :n:`@bullet__1` again, you should first finish proving + the current focused goal. + Note that :n:`@bullet__1` and :n:`@bullet__2` may be the same. -.. exn:: Wrong bullet @bullet1: Bullet @bullet2 is mandatory here. +.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here. - You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here. + You must put :n:`@bullet__2` to focus on the next goal. No other bullet is + allowed here. .. exn:: No such goal. Focus next goal with bullet @bullet. - You tried to apply a tactic but no goals were under focus. Using :n:`@bullet` is mandatory here. + You tried to apply a tactic but no goals were under focus. + Using :n:`@bullet` is mandatory here. .. exn:: No such goal. Try unfocusing with %{. @@ -433,7 +466,7 @@ Requesting information .. cmdv:: Show @num - Displays only the :token:`num` th subgoal. + Displays only the :token:`num`\-th subgoal. .. exn:: No such goal. |