diff options
| author | Pierre-Marie Pédrot | 2018-11-24 17:04:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-05 17:55:12 +0100 |
| commit | b8a082c940df58b03f45208a7a09ae36bf1f7634 (patch) | |
| tree | e02b437077c94faa99f89ba852b568438c2234e2 /gramlib/plexing.ml | |
| parent | 7f4da9fbbe568ea921845f145c21d036c08c328e (diff) | |
Remove the lexer field from Gramlib.
This is useless in the functorial API.
Diffstat (limited to 'gramlib/plexing.ml')
0 files changed, 0 insertions, 0 deletions