diff options
| author | Hugo Herbelin | 2015-04-18 10:16:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-04-20 12:18:01 +0200 |
| commit | b846c413c2e79520a5238c5a0775f5cd73d61bac (patch) | |
| tree | 1292d6af5857ab3e3075d19ae99aedf045725555 /dev/base_include | |
| parent | 738551a294d5d8393253568764f9bea4cf45f7c5 (diff) | |
Inlining "fun" and "forall" tokens in parser, so that alternative notations for
them (e.g. "fun ... ⇒ ...") factor well (see #2268).
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions