diff options
| author | Enrico Tassi | 2019-03-05 11:42:17 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-31 14:36:28 +0200 |
| commit | 912eaf40d4efd29b7e3489d51c55b8b79206df79 (patch) | |
| tree | b4793da97a5513d460c3d08721cb40692eeddd71 /kernel/nativelambda.ml | |
| parent | ed996432fd079583afbb1797c92ad23f654b94eb (diff) | |
[parsing] Split Tok.t into Tok.t and Tok.pattern
Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals
Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t
Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions
