diff options
| author | Pierre-Marie Pédrot | 2021-01-11 12:38:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-11 12:38:10 +0100 |
| commit | 10eb052719f22ee6d7a69588b7f8d7830e1cbd39 (patch) | |
| tree | ea8b5bb82b7f11221d0a27298a4f6fb1a8e6b430 /dev/ci | |
| parent | ffb482f0c18bff2c65dcc9cd2b65bd20b398245d (diff) | |
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.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions