Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)

Reviewed-by: CohenCyril
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot

6 files changed, 47 insertions, 17 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 3b4b80ca21..4eaca8634f 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
 
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 1c81fbc10b..1e182b52fa 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -485,17 +485,22 @@ let revtoptac n0 =
   Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))
   end
 
-let equality_inj l b id c =
-  Proofview.V82.tactic begin fun gl ->
-  let msg = ref "" in
-  try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
-  with
-    | CErrors.UserError (_,s)
-  when msg := Pp.string_of_ppcmds s;
-       !msg = "Not a projectable equality but a discriminable one." ||
-       !msg = "Nothing to inject." ->
-    Feedback.msg_warning (Pp.str !msg);
-    discharge_hyp (id, (id, "")) gl
+let nothing_to_inject =
+   CWarnings.create ~name:"spurious-ssr-injection" ~category:"ssr"
+     (fun (sigma, env, ty) ->
+         Pp.(str "SSReflect: cannot obtain new equations out of" ++ fnl() ++
+             str"  " ++ Printer.pr_econstr_env env sigma ty ++ fnl() ++
+             str "Did you write an extra [] in the intro pattern?"))
+
+let equality_inj l b id c = Proofview.Goal.enter begin fun gl ->
+  Proofview.tclORELSE (Equality.inj None l b None c)
+    (function
+    | (Equality.NothingToInject,_) ->
+        let open Proofview.Notations in
+        Ssrcommon.tacTYPEOF (EConstr.mkVar id) >>= fun ty ->
+        nothing_to_inject (Proofview.Goal.sigma gl, Proofview.Goal.env gl, ty);
+        Proofview.V82.tactic (discharge_hyp (id, (id, "")))
+    | (e,info) -> Proofview.tclZERO ~info e)
   end
 
 let injectidl2rtac id c =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a2325b69cc..1689b0d3ad 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1416,6 +1416,11 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
+exception NothingToInject
+let () = CErrors.register_handler (function
+  | NothingToInject -> Some (Pp.str "Nothing to inject.")
+  | _ -> None)
+
 let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
@@ -1429,7 +1434,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
             " You can try to use option Set Keep Proof Equalities." in
      tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
   | Inr [([],_,_)] ->
-     tclZEROMSG (str"Nothing to inject.")
+     Proofview.tclZERO NothingToInject
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
         (tac (clenv_value eq_clause))
diff --git a/tactics/equality.mli b/tactics/equality.mli
index e252eeab28..fdcbbc0e3c 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -91,6 +91,7 @@ val discr_tac    : evars_flag ->
   constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
 
 (* Below, if flag is [None], it takes the value from the dynamic value of the option *)
+exception NothingToInject
 val inj          : inj_flags option -> intro_patterns option -> evars_flag ->
   clear_flag -> constr with_bindings -> unit Proofview.tactic
 val injClause    : inj_flags option -> intro_patterns option -> evars_flag ->
diff --git a/test-suite/ssr/noting_to_inject.v b/test-suite/ssr/noting_to_inject.v
new file mode 100644
index 0000000000..95bbd3e777
--- /dev/null
+++ b/test-suite/ssr/noting_to_inject.v
@@ -0,0 +1,9 @@
+Require Import ssreflect ssrfun ssrbool.
+
+
+Goal forall b : bool, b -> False.
+Set Warnings "+spurious-ssr-injection".
+Fail move=> b [].
+Set Warnings "-spurious-ssr-injection".
+move=> b [].
+Abort.