diff options
Diffstat (limited to 'gramlib/plexing.mli')
| -rw-r--r-- | gramlib/plexing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index 6139dc4020..f6e4d96b80 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -28,7 +28,7 @@ type 'te lexer = tok_match : pattern -> 'te -> string; tok_text : pattern -> string; } -and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function +and 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function and location_function = int -> Loc.t (** The type of a function giving the location of a token in the source from the token number in the stream (starting from zero). *) |