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.

3 files changed, 38 insertions, 1 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index fe73b6105b..2090aad8a0 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -404,7 +404,9 @@ let rec pat_of_raw metas vars = function
 
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
-    | PatVar(_,na) -> na
+    | PatVar(_,na) ->
+      name_iter (fun n -> metas := n::!metas) na;
+      na
     | PatCstr(loc,_,_,_) -> err loc (Pp.str "Non supported pattern.")
   in
   let rec get_pat indexes = function
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