diff options
| author | Matthieu Sozeau | 2014-09-04 00:18:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-04 01:13:33 +0200 |
| commit | 593dfd66a5016ba457b6dccf1179a0e1ec7bff84 (patch) | |
| tree | f99ae900cc9b8e13b69ea1b75151f1679ce066d6 /kernel/declarations.mli | |
| parent | 8287733d5df1bd673a38e92f23c47e95d1bb7a91 (diff) | |
Fix bug #3563, making syntactic matching of primitive projections
and their eta-expanded forms succeed, potentially filling parameter
metavariables from the type information of the projected object.
Diffstat (limited to 'kernel/declarations.mli')
0 files changed, 0 insertions, 0 deletions