From 0aa3f871051c737192f9a19b79957b32b6ecafea Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 24 Jul 2020 16:01:57 +0200
Subject: [ssr] turn "nothing to inject" into a real warning (fix #12746)

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 14 +++++++++++++-
 doc/sphinx/proof-engine/tactics.rst                  |  6 ++----
 2 files changed, 15 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7b3670164b..09ce002e8c 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1211,6 +1211,8 @@ The move tactic.
    :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics.
 
 
+.. _the_case_tactic_ssr:
+
 The case tactic
 ```````````````
 
@@ -1235,7 +1237,17 @@ The case tactic
 
      x = 1 -> y = 2 -> G.
 
-   Note also that the case of |SSR| performs :g:`False` elimination, even
+   The :tacn:`case` can generate the following warning:
+
+   .. warn:: SSReflect: cannot obtain new equations out of ...
+
+      The tactic was run on an equation that cannot generate simpler equations,
+      for example `x = 1`.
+
+   The warning can be silenced or made fatal by using the :opt:`Warnings` option
+   and the `spurious-ssr-injection` key.
+
+   Finally the :tacn:`case` tactic of |SSR| performs :g:`False` elimination, even
    if no branch is generated by this case operation. Hence the tactic
    :tacn:`case` on a goal of the form :g:`False -> G` will succeed and
    prove the goal.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 25c4de7389..c5fab0983f 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2227,9 +2227,6 @@ and an explanation of the underlying technique.
       then :n:`injection @ident` first introduces the hypothesis in the local
       context using :n:`intros until @ident`.
 
-   .. exn:: Not a projectable equality but a discriminable one.
-      :undocumented:
-
    .. exn:: Nothing to do, it is an equality between convertible terms.
       :undocumented:
 
@@ -2237,7 +2234,8 @@ and an explanation of the underlying technique.
       :undocumented:
 
    .. exn:: Nothing to inject.
-      :undocumented:
+
+      This error is given when one side of the equality is not a constructor.
 
    .. tacv:: injection @num
 
-- 
cgit v1.2.3