diff options
| author | Pierre-Marie Pédrot | 2015-08-22 16:21:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-22 16:21:07 +0200 |
| commit | 2903ee1394118106f1894798f82dc5cf3730675b (patch) | |
| tree | 76a29b8da20b51b48c6a73516a6ae9c107f57afc /test-suite | |
| parent | 4c202177e7d1a26f3b8bc105a1ceb604f178b584 (diff) | |
| parent | 081a649157d2460c924404cd51b4ba50c23b1956 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4318.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4318.v b/test-suite/bugs/closed/4318.v new file mode 100644 index 0000000000..e3140ed5ab --- /dev/null +++ b/test-suite/bugs/closed/4318.v @@ -0,0 +1,2 @@ +(* Check no anomaly is raised *) +Fail Definition foo p := match p with (x, y) z => tt end. |