From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Mar 2017 02:18:53 +0100
Subject: A fix to #5414 (ident bound by ltac names now known for "match").

Also taking into account a name in the return clause and in the
indices.

Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
---
 test-suite/bugs/closed/5414.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test-suite/bugs/closed/5414.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5414.v b/test-suite/bugs/closed/5414.v
new file mode 100644
index 0000000000..2522a274fb
--- /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" *)
-- 
cgit v1.2.3