diff options
| author | Pierre-Marie Pédrot | 2019-02-05 17:50:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-11 15:48:43 +0100 |
| commit | 8c3bf38e574b576dfd5389ff012c7dbc969fc2ab (patch) | |
| tree | 999cd794df341ae7b850f9e89467c71dd9253f9f /Makefile.dev | |
| parent | 5c41d4feb28f181aa6a6a7c9624341eac5eda9d5 (diff) | |
Introduce a GADT of well-typed grammar entries in Grammar.
Not fully used yet, we rely on erasure casts for now.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions