1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5414.v b/test-suite/bugs/closed/5414.v
new file mode 100644
index 00000000..2522a274
--- /dev/null
+++ b/test-suite/bugs/closed/5414.v
@@ -0,0 +1,12 @@
+(* Use of idents bound to ltac names in a "match" *)
+
+Definition foo : Type.
+Proof.
+  let x := fresh "a" in
+  refine (forall k : nat * nat, let '(x, _) := k in (_ : Type)).
+  exact (a = a).
+Defined.
+Goal foo.
+intros k. elim k. (* elim because elim keeps names *)
+intros.
+Check a. (* We check that the name is "a" *)