diff options
| author | Hugo Herbelin | 2017-04-08 18:35:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-08 18:42:50 +0200 |
| commit | 007ab31b4d1b9457d2758a614aed5a49dee53b62 (patch) | |
| tree | 59044dde6e53ee4e812cca72e979a11d4069101f /test-suite | |
| parent | 48c44b55b76e75aa2af9f82753c6ffe7531790c8 (diff) | |
Fixing #5460 (limitation in computing deps in pattern-matching compilation).
This was assuming dependencies occurring in configurations of
the form x:A, y:B x, z:C x y |- match x, y, z with ... end".
But still work to do for better management of dependencies in general...
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/5460.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5460.v b/test-suite/bugs/closed/5460.v new file mode 100644 index 0000000000..50221cdd83 --- /dev/null +++ b/test-suite/bugs/closed/5460.v @@ -0,0 +1,11 @@ +(* Bugs in computing dependencies in pattern-matching compilation *) + +Inductive A := a1 | a2. +Inductive B := b. +Inductive C : A -> Type := c : C a1 | d : C a2. +Definition P (x : A) (y : C x) (z : B) : nat := + match z, x, y with + | b, a1, c => 0 + | b, a2, d => 0 + | _, _, _ => 1 + end. |