diff options
| author | herbelin | 2004-07-16 16:11:29 +0000 |
|---|---|---|
| committer | herbelin | 2004-07-16 16:11:29 +0000 |
| commit | 4c91b0075850a5cd245a7c5917d2e036afa18c13 (patch) | |
| tree | fc81e66165f81b6d122aa214ce1555a7ef92a055 | |
| parent | 9e7cf06884565e3db81f63555ae259dbddcfe89d (diff) | |
Branchement sur Util.loc et abstraction vis a vis de dummy_loc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5912 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 = |