setoid_rewrite: record generated name when rewriting under lambda

Fix #13129

2 files changed, 62 insertions, 0 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e69bfc2741..82ef4b494e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1120,6 +1120,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 
       | Lambda (n, t, b) when flags.under_lambdas ->
         let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
+        let unfresh = match n'.binder_name with
+          | Anonymous -> unfresh
+          | Name id -> Id.Set.add id unfresh
+        in
         let open Context.Rel.Declaration in
         let env' = EConstr.push_rel (LocalAssum (n', t)) env in
         let bty = Retyping.get_type_of env' (goalevars evars) b in
diff --git a/test-suite/bugs/closed/bug_13129.v b/test-suite/bugs/closed/bug_13129.v
new file mode 100644
index 0000000000..632605ecc7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13129.v
@@ -0,0 +1,58 @@
+From Coq Require Export Morphisms Setoid .
+
+Class Equiv A := equiv: relation A.
+
+Infix "≡" := equiv (at level 70, no associativity).
+Infix "≡@{ A }" := (@equiv A _)
+  (at level 70, only parsing, no associativity).
+
+Notation "(≡)" := equiv (only parsing).
+
+(** Unbundled version *)
+Class Dist A := dist : nat -> relation A.
+
+Notation "x ≡{ n }≡ y" := (dist n x y)
+  (at level 70, n at next level, format "x  ≡{ n }≡  y").
+Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
+  (at level 70, n at next level, only parsing).
+
+Notation NonExpansive f := (forall n, Proper (dist n ==> dist n ==> dist n) f).
+
+Record OfeMixin A `{Equiv A, Dist A} := {
+  mixin_equiv_dist (x y : A) : x ≡ y <-> forall n, x ≡{n}≡ y;
+}.
+
+(** Bundled version *)
+Structure ofeT := OfeT {
+  ofe_car :> Type;
+  ofe_equiv : Equiv ofe_car;
+  ofe_dist : Dist ofe_car;
+  ofe_mixin : OfeMixin ofe_car
+}.
+Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
+Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
+
+(** Lifting properties from the mixin *)
+Section ofe_mixin.
+  Context {A : ofeT}.
+  Implicit Types x y : A.
+  Lemma equiv_dist x y : x ≡ y <-> forall n, x ≡{n}≡ y.
+  Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
+End ofe_mixin.
+
+Axiom _0 : Prop. (* dummy which somehow bothers mangle names *)
+Set Mangle Names.
+
+(** General properties *)
+Section ofe.
+  Context {A : ofeT}.
+
+  Lemma ne_proper_2 {B C : ofeT} (f : A -> B -> C) `{Hf:!NonExpansive f} :
+    Proper ((≡) ==> (≡) ==> (≡)) f.
+  Proof.
+    unfold Proper, respectful.
+    setoid_rewrite equiv_dist.
+    intros.
+    apply Hf;auto.
+  Qed.
+End ofe.