From 5bda981276517983a042e635c1fd1d12d8ad77af Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 28 Mar 2020 18:00:21 +0100
Subject: Document change of behavior of Fail in 8.11.

---
 doc/sphinx/changes.rst                          |  4 ++++
 doc/sphinx/proof-engine/vernacular-commands.rst | 17 +++++++++--------
 2 files changed, 13 insertions(+), 8 deletions(-)

(limited to 'doc')

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:
-- 
cgit v1.2.3