diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml4 | 6 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 3 |
2 files changed, 0 insertions, 9 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 5fcbb43b6f..636027f9b4 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -368,9 +368,6 @@ let rec string loc ~comm_level bp len = parser let loc = set_loc_pos loc bp ep in err loc Unterminated_string -(* Hook for exporting comment into xml theory files *) -let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () - (* To associate locations to a file name *) let current_file = ref None @@ -432,9 +429,6 @@ let null_comment s = let comment_stop ep = let current_s = Buffer.contents current_comment in - if !Flags.xml_export && Buffer.length current_comment > 0 && - (!between_commands || not(null_comment current_s)) then - Hook.get f_xml_output_comment current_s; (if !Flags.beautify && Buffer.length current_comment > 0 && (!between_commands || not(null_comment current_s)) then let bp = match !comment_begin with diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 09c9d8ee45..77d652b185 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: *) |