From 0c1265f56a46e79aac85ae2c08cd6261141b0788 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Oct 2020 14:47:13 +0200
Subject: setoid_rewrite: record generated name when rewriting under lambda

Fix #13129
---
 plugins/ltac/rewrite.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins')

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
-- 
cgit v1.2.3