Merge PR#507: Intern names bound in match patterns

2 files changed, 35 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5345.v b/test-suite/bugs/closed/5345.v
new file mode 100644
index 000000000..d8448f35d
--- /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 000000000..736329496
--- /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