summaryrefslogtreecommitdiff
path: root/parsing/lexer.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/lexer.mli')
-rw-r--r--parsing/lexer.mli12
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