Merge PR #12508: Fix #12507 Anomaly when using a ssreflect `reflect` view

Reviewed-by: CohenCyril
Reviewed-by: ppedrot

2 files changed, 38 insertions, 4 deletions

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 29a9c65561..da623703a2 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -389,17 +389,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
   try Proofview.V82.of_tactic (refine_with
     ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl
-  with _ ->
+  with e when CErrors.noncritical e ->
     (* we generate a msg like: "Unable to find an instance for the variable" *)
     let hd_ty, miss = match EConstr.kind sigma c with
     | App (hd, args) ->
         let hd_ty = Retyping.get_type_of env sigma hd in
-        let names = let rec aux t = function 0 -> [] | n ->
+        let names = let rec aux env t = function 0 -> [] | n ->
           let t = Reductionops.whd_all env sigma t in
           let open EConstr in
           match kind_of_type sigma t with
-          | ProdType (name, _, t) -> name.binder_name :: aux t (n-1)
-          | _ -> assert false in aux hd_ty (Array.length args) in
+          | ProdType (name, ty, t) ->
+              name.binder_name ::
+                aux (EConstr.push_rel (Context.Rel.Declaration.LocalAssum (name,ty)) env) t (n-1)
+          | _ ->
+              (* In the case the head is an HO constant it may accept more arguments *)
+              CList.init n (fun _ -> Names.Name.Anonymous) in aux env hd_ty (Array.length args) in
         hd_ty, Util.List.map_filter (fun (t, name) ->
           let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in
           let open_evs = List.filter (fun k ->
diff --git a/test-suite/ssr/rewrtite_err_msg.v b/test-suite/ssr/rewrtite_err_msg.v
new file mode 100644
index 0000000000..2bbbff433c
--- /dev/null
+++ b/test-suite/ssr/rewrtite_err_msg.v
@@ -0,0 +1,30 @@
+Require Import ssreflect ssrbool.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Axiom finGroupType : Type.
+Axiom group : finGroupType -> Type.
+Axiom abelian : forall gT : finGroupType, group gT -> Prop.
+Arguments abelian {_} _.
+Axiom carrier : finGroupType -> Type.
+Coercion carrier : finGroupType >-> Sortclass.
+Axiom mem : forall gT : finGroupType, gT -> group gT -> Prop.
+Arguments mem {_} _ _.
+Axiom mul : forall gT : finGroupType, gT -> gT -> gT.
+Arguments mul {_} _ _.
+Definition centralised gT (G : group gT) (x : gT) := forall y, mul x y = mul y x.
+Arguments centralised {gT} _.
+Axiom b : bool.
+
+Axiom centsP : forall (gT : finGroupType) (A B : group gT),
+  reflect (forall a, mem a A -> centralised B a) b.
+Arguments centsP {_ _ _}.
+
+Lemma commute_abelian (gT : finGroupType) (G : group gT)
+  (G_abelian : abelian G) (g g' : gT) (gG : mem g  G) (g'G : mem g'  G) :
+  mul g g' = mul g' g.
+Proof.
+Fail rewrite (centsP _). (* fails but without an anomaly *)
+Abort.