aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Zeimer <zzaimer@gmail.com>2018-07-20 18:56:43 +0200
committerGravatar Zeimer <zzaimer@gmail.com>2018-07-20 18:57:32 +0200
commitb2bdaad8567e3ca91e036268a042129b6ce6f987 (patch)
tree6880c2bf0ebbf496e374f8a1476bb59d5e615dec /doc
parent3eeb4fb840328a0f8831c402b2347196bfa0042d (diff)
Small improvements suggested in comments to PR #8086.
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/proof-engine/ltac.rst14
1 files changed, 13 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 90b44da00..dc355fa01 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -572,7 +572,9 @@ Failing
.. tacv:: gfail
:name: gfail
- This variant fails when used after :n:`;` even if there are no goals left (see the example).
+ This variant fails even when used after :n:`;` and there are no goals left.
+ Similarly, ``gfail`` fails even when used after ``all:`` and there are no
+ goals left. See the example for clarification.
.. tacv:: gfail {* message_token}
@@ -603,6 +605,9 @@ Failing
Proof. trivial. fail. Abort.
Goal True.
+ Proof. trivial. all: fail. Qed.
+
+ Goal True.
Proof. gfail. Abort.
Goal True.
@@ -611,6 +616,9 @@ Failing
Goal True.
Proof. trivial. gfail. Abort.
+ Goal True.
+ Proof. trivial. all: gfail. Abort.
+
Timeout
~~~~~~~
@@ -921,7 +929,10 @@ produce subgoals but generates a term to be used in tactic expressions:
value of :n:`@ident` by the value of :n:`@expr`.
.. exn:: Not a context variable.
+ :undocumented:
+
.. exn:: Unbound context identifier @ident.
+ :undocumented:
Generating fresh hypothesis names
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1212,6 +1223,7 @@ following:
+-----------------+-----------------------------------------------+
.. exn:: Debug mode not available in the IDE
+ :undocumented:
A non-interactive mode for the debugger is available via the option: