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/grammar.mli | |
| parent | 7f4da9fbbe568ea921845f145c21d036c08c328e (diff) | |
Remove the lexer field from Gramlib.
This is useless in the functorial API.
Diffstat (limited to 'gramlib/grammar.mli')
| -rw-r--r-- | gramlib/grammar.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 4b61286859..bde07ddc48 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -25,7 +25,6 @@ module type S = type parsable val parsable : char Stream.t -> parsable val tokens : string -> (string * int) list - val glexer : te Plexing.lexer module Entry : sig type 'a e |