diff options
| author | Clément Pit-Claudel | 2020-03-28 16:56:23 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-03-28 16:56:23 -0400 |
| commit | eb01bc0f7583ef958a32e88c05d82cb9ad791ac4 (patch) | |
| tree | 7e02896f5525b58f1120f65bec7e7db7eb431c40 | |
| parent | 28081c1108a84050566d365bd665d05ee508ecce (diff) | |
| parent | 5bda981276517983a042e635c1fd1d12d8ad77af (diff) | |
Merge PR #11950: Document change of behavior of Fail in 8.11.
| -rw-r--r-- | doc/sphinx/changes.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 17 |
2 files changed, 13 insertions, 8 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5ca0d8b81f..7401aff48c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -383,6 +383,10 @@ Changes in 8.11+beta1 <https://github.com/coq/coq/issues/3890>`_ and `#4638 <https://github.com/coq/coq/issues/4638>`_ by Maxime Dénès, review by Gaëtan Gilbert). +- **Changed:** + :cmd:`Fail` does not catch critical errors (including "stack overflow") + anymore (`#10173 <https://github.com/coq/coq/pull/10173>`_, + by Gaëtan Gilbert). - **Removed:** Undocumented :n:`Instance : !@type` syntax (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c33d62532e..2ca115aeb8 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -929,16 +929,17 @@ Quitting and debugging .. cmd:: Fail @command - For debugging scripts, sometimes it is desirable to know - whether a command or a tactic fails. If the given :n:`@command` - fails, the ``Fail`` statement succeeds, without changing the proof - state, and in interactive mode, the system - prints a message confirming the failure. - If the given :n:`@command` succeeds, the statement is an error, and - it prints a message indicating that the failure did not occur. + For debugging scripts, sometimes it is desirable to know whether a + command or a tactic fails. If the given :n:`@command` fails, then + :n:`Fail @command` succeeds (excepts in the case of + critical errors, like a "stack overflow"), without changing the + proof state, and in interactive mode, the system prints a message + confirming the failure. .. exn:: The command has not failed! - :undocumented: + + If the given :n:`@command` succeeds, then :n:`Fail @command` + fails with this error message. .. _controlling-display: |