diff options
author | 2015-03-03 22:28:09 +0100 | |
---|---|---|
committer | 2015-03-03 22:28:09 +0100 | |
commit | f51efdd18b01c7f3fce026c32c0cd21ff4f6ca02 (patch) | |
tree | e2525dc3f06393b9fe6c7850edbcdb7991c56c6d /test-suite/bugs/closed/1907.v | |
parent | c135410086c256fcc74f579459687a83718148b9 (diff) |
Add a test-suite file ensuring coinductives with primitive projections
do not enjoy eta-conversion and do not allow the usual failure of
subject reduction in presence of dependent pattern-matching.
Diffstat (limited to 'test-suite/bugs/closed/1907.v')
0 files changed, 0 insertions, 0 deletions