From b1656b1f10501b34ae6a7e147f550710b935e54b Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Wed, 22 Mar 2017 20:35:38 -0400
Subject: Intern names bound in match patterns

Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
---
 test-suite/bugs/closed/5345.v                 |  7 +++++++
 test-suite/success/ltac_match_pattern_names.v | 28 +++++++++++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 test-suite/bugs/closed/5345.v
 create mode 100644 test-suite/success/ltac_match_pattern_names.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5345.v b/test-suite/bugs/closed/5345.v
new file mode 100644
index 0000000000..d8448f35db
--- /dev/null
+++ b/test-suite/bugs/closed/5345.v
@@ -0,0 +1,7 @@
+Ltac break_tuple :=
+  match goal with
+  | [ H: context[match ?a with | pair n m => _ end] |- _ ] =>
+    let n := fresh n in
+    let m := fresh m in
+    destruct a as [n m]
+  end.
diff --git a/test-suite/success/ltac_match_pattern_names.v b/test-suite/success/ltac_match_pattern_names.v
new file mode 100644
index 0000000000..7363294960
--- /dev/null
+++ b/test-suite/success/ltac_match_pattern_names.v
@@ -0,0 +1,28 @@
+(* example from bug 5345 *)
+Ltac break_tuple :=
+  match goal with
+  | [ H: context[let '(n, m) := ?a in _] |- _ ] =>
+    let n := fresh n in
+    let m := fresh m in
+    destruct a as [n m]
+  end.
+
+(* desugared version of break_tuple *)
+Ltac break_tuple' :=
+  match goal with
+  | [ H: context[match ?a with | pair n m => _ end] |- _ ] =>
+    let n := fresh n in
+    let m := fresh m in
+    idtac
+  end.
+
+Ltac multiple_branches :=
+  match goal with
+  | [ H: match _ with
+         | left P => _
+         | right Q => _
+         end |- _ ] =>
+    let P := fresh P in
+    let Q := fresh Q in
+    idtac
+  end.
\ No newline at end of file
-- 
cgit v1.2.3