diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 22:12:02 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-08-01 18:42:44 +0200 |
commit | 2def58217686b5083da38778a5ebffb451b1d4d6 (patch) | |
tree | c0c2463a4620fe3c6bb2caf21a70f6861bbb4643 /parsing/cLexer.mli | |
parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) |
[flags] Remove XML output flag.
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
Diffstat (limited to 'parsing/cLexer.mli')
-rw-r--r-- | parsing/cLexer.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 09c9d8ee4..77d652b18 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -19,9 +19,6 @@ val get_keyword_state : unit -> keyword_state val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit - -val xml_output_comment : (string -> unit) Hook.t - val terminal : string -> Tok.t (** The lexer of Coq: *) |