From f6a8c2542a5ce85a91caf9b1745c980c2164707a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 12 Nov 2020 14:36:02 +0100
Subject: Fix incorrect name refreshing when interning a generalized binder

Fix #13249
---
 interp/constrintern.ml             | 22 +++++++++++++---------
 test-suite/bugs/closed/bug_13249.v |  9 +++++++++
 2 files changed, 22 insertions(+), 9 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_13249.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 02c3c047d5..c4b5bf8984 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -534,15 +534,19 @@ let intern_generalized_binder intern_type ntnvars
   in
   let na = match na with
     | Anonymous ->
-          let name =
-            let id =
-              match ty with
-              | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
-                qualid_basename qid
-              | _ -> default_non_dependent_ident
-            in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
-          in Name name
-    | _ -> na in
+      let id =
+        match ty with
+        | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
+          qualid_basename qid
+        | _ -> default_non_dependent_ident
+      in
+      let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in
+      let id =
+        Implicit_quantifiers.make_fresh ids' (Global.env ()) id
+      in
+      Name id
+    | _ -> na
+  in
   let impls = impls_type_list 1 ty' in
   (push_name_env ntnvars impls env' (make ?loc na),
    (make ?loc (na,b',ty')) :: List.rev bl)
diff --git a/test-suite/bugs/closed/bug_13249.v b/test-suite/bugs/closed/bug_13249.v
new file mode 100644
index 0000000000..06f7ddbd3a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13249.v
@@ -0,0 +1,9 @@
+Global Generalizable All Variables.
+
+Section test.
+  Context {A : Type}.
+  Context `{!foo A}.
+
+  Goal foo A.
+  Proof. assumption. Defined.
+End test.
-- 
cgit v1.2.3