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".

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 000000000..2522a274f
--- /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" *)