diff options
Diffstat (limited to 'parsing/lexer.mli')
| -rw-r--r-- | parsing/lexer.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 95eadfcb6..66a04a194 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -12,7 +12,7 @@ val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool -val location_function : int -> loc +val location_function : int -> Loc.t (** for coqdoc *) type location_table |