diff options
| author | Matthieu Sozeau | 2014-08-08 15:33:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-08 15:33:06 +0200 |
| commit | ff884c172697c1452db535cdbd6babceb556c428 (patch) | |
| tree | ac7092faa6368ff85eacc68385c67b118b0280d4 /kernel | |
| parent | 758f031bc2e2d4a5ece6d515533fafe3e9df98d5 (diff) | |
Change internalization of primitive projections to allow parsing [p t] as
a primitive application only if all parameters of [p] are implicit, falling
back to the internalization of the eta-expanded version otherwise. This makes
apply [p] succeed even if its record argument is not implicit, ensuring better
compatibility.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions