aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/parsing.mllib
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-07-25 17:52:46 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-07-25 17:56:06 +0200
commit3f7f3a9bc9fde8e1d44d1179fa8dd16221ebf526 (patch)
treee40711bfad4132309b527c2c6c63b2bb5a61d1f2 /parsing/parsing.mllib
parentafe396e1e2d2fee621d96e7cbc950b0a28bd9606 (diff)
- Do module substitution inside mind_record.
- Distinguish between primitive and non-primitive records in the kernel declaration, so as to try eta-conversion on primitive records only.
Diffstat (limited to 'parsing/parsing.mllib')
0 files changed, 0 insertions, 0 deletions