diff options
| -rw-r--r-- | parsing/egrammar.mli | 1 | ||||
| -rw-r--r-- | parsing/lexer.mli | 5 | ||||
| -rw-r--r-- | parsing/q_util.ml4 | 2 |
3 files changed, 5 insertions, 3 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 47b8beced3..84809265a6 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -9,6 +9,7 @@ (*i $Id$ i*) (*i*) +open Util open Topconstr open Ast open Coqast diff --git a/parsing/lexer.mli b/parsing/lexer.mli index a992522b1e..c6825283d0 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -9,6 +9,7 @@ (*i $Id$ i*) open Pp +open Util type error = | Illegal_character @@ -22,8 +23,8 @@ exception Error of error val add_token : string * string -> unit val is_keyword : string -> bool -val func : char Stream.t -> (string * string) Stream.t * (int -> int * int) -val location_function : int -> int * int +val func : char Stream.t -> (string * string) Stream.t * (int -> loc) +val location_function : int -> loc (* for coqdoc *) type location_table diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 5dcb0686da..540d681aa2 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -10,7 +10,7 @@ (* This file defines standard combinators to build ml expressions *) -let dummy_loc = (0,0) +open Util let not_impl name x = let desc = |