From b2bdaad8567e3ca91e036268a042129b6ce6f987 Mon Sep 17 00:00:00 2001 From: Zeimer Date: Fri, 20 Jul 2018 18:56:43 +0200 Subject: Small improvements suggested in comments to PR #8086. --- doc/sphinx/proof-engine/ltac.rst | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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} @@ -602,6 +604,9 @@ Failing Goal True. Proof. trivial. fail. Abort. + Goal True. + Proof. trivial. all: fail. Qed. + Goal True. Proof. gfail. Abort. @@ -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: -- cgit v1.2.3