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
---
 test-suite/bugs/closed/bug_13249.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13249.v

(limited to 'test-suite')

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