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.mli | |
| 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.mli')
| -rw-r--r-- | parsing/cLexer.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 3ad49eb74..71edda760 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -10,14 +10,6 @@ val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool -(* val location_function : int -> Loc.t *) - -(** for coqdoc *) -type location_table -val location_table : unit -> location_table -val restore_location_table : location_table -> unit - - (** [get_current_file fname] returns the filename used in locations emitted by the lexer *) val get_current_file : unit -> string |