From 10eb052719f22ee6d7a69588b7f8d7830e1cbd39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Jan 2021 12:38:10 +0100
Subject: 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.
---
 test-suite/success/let_pattern_mismatch.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/success/let_pattern_mismatch.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3