diff options
| author |  Zeimer <zzaimer@gmail.com> | 2018-07-20 18:56:43 +0200 |
|---|---|---|
| committer | Zeimer <zzaimer@gmail.com> | 2018-07-20 18:57:32 +0200 |
| commit | b2bdaad8567e3ca91e036268a042129b6ce6f987 (patch) | |
| tree | 6880c2bf0ebbf496e374f8a1476bb59d5e615dec | |
| parent | 3eeb4fb840328a0f8831c402b2347196bfa0042d (diff) | |
Small improvements suggested in comments to PR #8086.
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 14 |
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: |