3 files changed, 19 insertions, 14 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1b7768852e..d859fe51ab 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1047,7 +1047,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc =
   let uct = Evd.evar_universe_context (fst oc) in
   let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
   Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*>
-  Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
+  Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
     (fun _ -> Proofview.tclZERO dependent_apply_error)
   end
 
@@ -1352,7 +1352,7 @@ let unsafe_intro env decl b =
   Refine.refine ~typecheck:false begin fun sigma ->
     let ctx = Environ.named_context_val env in
     let nctx = EConstr.push_named_context_val decl ctx in
-    let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
+    let inst = EConstr.identity_subst_val (Environ.named_context_val env) in
     let ninst = EConstr.mkRel 1 :: inst in
     let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
     let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in
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/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index da623703a2..38b26d06b9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -465,7 +465,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr =
       Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0
   in
   let cvtac' =
-    Proofview.tclOR cvtac begin function
+    Proofview.tclORELSE cvtac begin function
     | (PRtype_error e, _) ->
       let error = Option.cata (fun (env, sigma, te) ->
           Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te))