diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 03:17:25 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:00 -0400 |
| commit | 767ecfec49543b70a605d20b1dae8252e1faabfe (patch) | |
| tree | 2b91f76b9f6c5148c7ba5e2b7cab14218d569259 /gramlib/grammar.ml | |
| parent | 13929f39f8560cfcb3aacf20c84c6dcb5295cec5 (diff) | |
[parsing] Make grammar rules private.
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
Diffstat (limited to 'gramlib/grammar.ml')
0 files changed, 0 insertions, 0 deletions