aboutsummaryrefslogtreecommitdiff
path: root/gramlib/plexing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'gramlib/plexing.ml')
-rw-r--r--gramlib/plexing.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index fce5445ad8..c294923a85 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -5,7 +5,7 @@
type pattern = string * string
type location_function = int -> Loc.t
-type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
+type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
type 'te lexer =
{ tok_func : 'te lexer_func;