2 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/success/let_pattern_mismatch.v b/test-suite/success/let_pattern_mismatch.v
new file mode 100644
index 0000000000..a56a8fff4f
--- /dev/null
+++ b/test-suite/success/let_pattern_mismatch.v
@@ -0,0 +1,18 @@
+(* Weird corner case accepted by the pattern-matching algorithm. Destructuring
+   let-bindings in patterns can actually be shorter than the case they match. *)
+
+Inductive ascii : Set :=
+| Ascii : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii.
+
+Definition dummy (a : ascii) : unit :=
+  let (a0,a1,a2,a3,a4,a5,a6,a7) := a in tt.
+
+Goal forall (a : ascii) (H : tt = dummy a), True.
+Proof.
+intros a H.
+unfold dummy in *.
+(* Two bound variables in the pattern, eight in the term. *)
+match goal with
+| H:context [ let (x, y) := ?X in _ ] |- _ => destruct X eqn:?
+end.
+Abort.
diff --git a/test-suite/success/match_case_pattern_variables.v b/test-suite/success/match_case_pattern_variables.v
new file mode 100644
index 0000000000..bb9117d033
--- /dev/null
+++ b/test-suite/success/match_case_pattern_variables.v
@@ -0,0 +1,34 @@
+(** Check that bound variables in case patterns are handled correctly. *)
+
+Goal forall (ch : unit) (t : list unit) (s : list unit),
+  match s with
+  | nil => False
+  | cons a l => ch = a /\ l = t
+  end.
+Proof.
+intros.
+match goal with
+| |- match ?e with
+    | nil => ?N
+    | cons a b => ?P
+    end =>
+     let f :=
+      constr:((fun (e' : list unit) => match e' with
+                          | nil => N
+                          | cons a b => P
+                          end))
+     in
+     change (f e)
+end.
+Abort.
+
+Goal forall (ch : unit) (n : nat) (s : prod unit nat),
+  let (a, l) := s in ch = a /\ l = n.
+Proof.
+intros.
+match goal with
+| [ |- let (a, b) := ?e in ?P ] =>
+  let f := constr:((fun (e' : prod unit nat) => match e' with pair a b => P end)) in
+  change (f e)
+end.
+Abort.