Add a test for a weird behaviour of tactic matching.

The arity of a destructuring let in a pattern is allowed to be shorter than
the case term node it actually matches. This is an unexpected side-effect
of the legacy expanded representation of cases that happens to be relied
upon in the wild, as evidenced by the CI failures from #13723.

1 files changed, 18 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.