aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-03-03 22:28:09 +0100
committerMatthieu Sozeau2015-03-03 22:28:09 +0100
commitf51efdd18b01c7f3fce026c32c0cd21ff4f6ca02 (patch)
treee2525dc3f06393b9fe6c7850edbcdb7991c56c6d /plugins
parentc135410086c256fcc74f579459687a83718148b9 (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 'plugins')
0 files changed, 0 insertions, 0 deletions