diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-11 12:58:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 20:14:13 +0200 |
| commit | 4e31561f7e0d5e647e86978806cae82ffb35f90b (patch) | |
| tree | ca7f7540c690bd40c5e29fcd3c8cde7c257ff9a6 /parsing/cLexer.ml4 | |
| parent | e4fcf8f9af193f125eb6ee101e739ba4460bd8b8 (diff) | |
Removing export of location_table outside of cLexer.
It was not used any more by coqdoc since b8194b22 (Dec 2010).
The table is now only part of the lexer function closure
(and only in the camlp5 case).
Diffstat (limited to 'parsing/cLexer.ml4')
| -rw-r--r-- | parsing/cLexer.ml4 | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 181c4b7fd..0090117f6 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -626,12 +626,6 @@ let loct_func loct i = let loct_add loct i loc = Hashtbl.add loct i loc -let current_location_table = ref (loct_create ()) - -type location_table = (int, Compat.CompatLoc.t) Hashtbl.t -let location_table () = !current_location_table -let restore_location_table t = current_location_table := t - (** {6 The lexer of Coq} *) (** Note: removing a token. @@ -669,7 +663,6 @@ let func cs = cur_loc := Compat.after loc; loct_add loct i loc; Some tok) in - current_location_table := loct; (ts, loct_func loct) let lexer = { @@ -706,7 +699,6 @@ end let mk () = let loct = loct_create () in let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in - current_location_table := loct; let rec self init_loc (* FIXME *) = parser i [< (tok, loc) = next_token !cur_loc; s >] -> |