diff options
Diffstat (limited to 'parsing/lexer.mli')
-rw-r--r-- | parsing/lexer.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/parsing/lexer.mli b/parsing/lexer.mli index f1ab6446..1b40d7f1 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lexer.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id$ i*) open Pp open Util @@ -21,9 +21,9 @@ type error = exception Error of error val add_token : string * string -> unit +val remove_keyword : string -> unit val is_keyword : string -> bool -val func : char Stream.t -> (string * string) Stream.t * (int -> loc) val location_function : int -> loc (* for coqdoc *) @@ -34,10 +34,6 @@ val restore_location_table : location_table -> unit val check_ident : string -> unit val check_keyword : string -> unit -val tparse : string * string -> ((string * string) Stream.t -> string) option - -val token_text : string * string -> string - type frozen_t val freeze : unit -> frozen_t val unfreeze : frozen_t -> unit @@ -50,3 +46,7 @@ val restore_com_state: com_state -> unit val set_xml_output_comment : (string -> unit) -> unit val terminal : string -> string * string + +(* The lexer of Coq *) + +val lexer : Compat.lexer |