diff options
Diffstat (limited to 'gramlib/grammar.ml')
| -rw-r--r-- | gramlib/grammar.ml | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 814844508b..834850082e 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -8,19 +8,6 @@ open Util (* Functorial interface *) -module type GLexerType = sig - include Plexing.Lexer - - module State : sig - type t - val init : unit -> t - val set : t -> unit - val get : unit -> t - val drop : unit -> unit - val get_comments : t -> ((int * int) * string) list - end -end - type norec type mayrec @@ -115,7 +102,7 @@ end (* Implementation *) -module GMake (L : GLexerType) = struct +module GMake (L : Plexing.S) = struct type te = L.te type 'c pattern = 'c L.pattern |