diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 22:28:09 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 22:28:09 +0100 |
| commit | f51efdd18b01c7f3fce026c32c0cd21ff4f6ca02 (patch) | |
| tree | e2525dc3f06393b9fe6c7850edbcdb7991c56c6d /.gitignore | |
| 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 '.gitignore')
0 files changed, 0 insertions, 0 deletions