From 2e53445be16ef28058599fed3f06424db17f6943 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 May 2020 15:52:47 +0200
Subject: Add test for #11727, which was indirectly fixed by this PR.

---
 test-suite/bugs/closed/bug_11727.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11727.v

diff --git a/test-suite/bugs/closed/bug_11727.v b/test-suite/bugs/closed/bug_11727.v
new file mode 100644
index 0000000000..d346f05c10
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11727.v
@@ -0,0 +1,8 @@
+Tactic Notation "myunfold" reference(x) := unfold x.
+Notation idnat := (@id nat).
+Goal let n := 0 in idnat n = 0.
+Proof.
+  intro n.
+  myunfold idnat.
+  myunfold n.
+Abort.
-- 
cgit v1.2.3