1 files changed, 0 insertions, 167 deletions
diff --git a/grammar/coqpp_lex.mll b/grammar/coqpp_lex.mll
deleted file mode 100644
index 6c6562c20..000000000
--- a/grammar/coqpp_lex.mll
+++ /dev/null
@@ -1,167 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-{
-
-open Lexing
-open Coqpp_parse
-
-type mode =
-| OCaml
-| Extend
-
-exception Lex_error of Coqpp_ast.loc * string
-
-let loc lexbuf = {
-  Coqpp_ast.loc_start = lexeme_start_p lexbuf;
-  Coqpp_ast.loc_end = lexeme_end_p lexbuf;
-}
-
-let newline lexbuf =
-  let pos = lexbuf.lex_curr_p in
-  let pos = { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum } in
-  lexbuf.lex_curr_p <- pos
-
-let num_comments = ref 0
-let num_braces = ref 0
-
-let mode () = if !num_braces = 0 then Extend else OCaml
-
-let comment_buf = Buffer.create 512
-let ocaml_buf = Buffer.create 512
-let string_buf = Buffer.create 512
-
-let lex_error lexbuf msg =
-  raise (Lex_error (loc lexbuf, msg))
-
-let lex_unexpected_eof lexbuf where =
-  lex_error lexbuf (Printf.sprintf "Unexpected end of file in %s" where)
-
-let start_comment _ =
-  let () = incr num_comments in
-  Buffer.add_string comment_buf "(*"
-
-let end_comment lexbuf =
-  let () = decr num_comments in
-  let () = Buffer.add_string comment_buf "*)" in
-  if !num_comments < 0 then lex_error lexbuf "Unexpected end of comment"
-  else if !num_comments = 0 then
-    let s = Buffer.contents comment_buf in
-    let () = Buffer.reset comment_buf in
-    Some (COMMENT s)
-  else
-    None
-
-let start_ocaml _ =
-  let () = match mode () with
-  | OCaml -> Buffer.add_string ocaml_buf "{"
-  | Extend -> ()
-  in
-  incr num_braces
-
-let end_ocaml lexbuf =
-  let () = decr num_braces in
-  if !num_braces < 0 then lex_error lexbuf "Unexpected end of OCaml code"
-  else if !num_braces = 0 then
-    let s = Buffer.contents ocaml_buf in
-    let () = Buffer.reset ocaml_buf in
-    Some (CODE { Coqpp_ast.code = s })
-  else
-    let () = Buffer.add_string ocaml_buf "}" in
-    None
-
-}
-
-let letter = ['a'-'z' 'A'-'Z']
-let letterlike = ['_' 'a'-'z' 'A'-'Z']
-let alphanum = ['_' 'a'-'z' 'A'-'Z' '0'-'9' '\'']
-let ident = letterlike alphanum*
-let qualid = ident ('.' ident)*
-let space = [' ' '\t' '\r']
-let number = [ '0'-'9' ]
-
-rule extend = parse
-| "(*" { start_comment (); comment lexbuf }
-| "{" { start_ocaml (); ocaml lexbuf }
-| "GRAMMAR" { GRAMMAR }
-| "VERNAC" { VERNAC }
-| "TACTIC" { TACTIC }
-| "EXTEND" { EXTEND }
-| "END" { END }
-| "DECLARE" { DECLARE }
-| "PLUGIN" { PLUGIN }
-(** Camlp5 specific keywords *)
-| "GLOBAL" { GLOBAL }
-| "FIRST" { FIRST }
-| "LAST" { LAST }
-| "BEFORE" { BEFORE }
-| "AFTER" { AFTER }
-| "LEVEL" { LEVEL }
-| "LEFTA" { LEFTA }
-| "RIGHTA" { RIGHTA }
-| "NONA" { NONA }
-(** Standard *)
-| ident { IDENT (Lexing.lexeme lexbuf) }
-| qualid { QUALID (Lexing.lexeme lexbuf) }
-| number { INT (int_of_string (Lexing.lexeme lexbuf)) }
-| space { extend lexbuf }
-| '\"' { string lexbuf }
-| '\n' { newline lexbuf; extend lexbuf }
-| '[' { LBRACKET }
-| ']' { RBRACKET }
-| '|' { PIPE }
-| "->" { ARROW }
-| ',' { COMMA }
-| ':' { COLON }
-| ';' { SEMICOLON }
-| '(' { LPAREN }
-| ')' { RPAREN }
-| '=' { EQUAL }
-| _ { lex_error lexbuf "syntax error" }
-| eof { EOF }
-
-and ocaml = parse
-| "{" { start_ocaml (); ocaml lexbuf }
-| "}" { match end_ocaml lexbuf with Some tk -> tk | None -> ocaml lexbuf }
-| '\n' { newline lexbuf; Buffer.add_char ocaml_buf '\n'; ocaml lexbuf }
-| '\"' { Buffer.add_char ocaml_buf '\"'; ocaml_string lexbuf }
-| (_ as c) { Buffer.add_char ocaml_buf c; ocaml lexbuf }
-| eof { lex_unexpected_eof lexbuf "OCaml code" }
-
-and comment = parse
-| "*)" { match end_comment lexbuf with Some _ -> extend lexbuf | None -> comment lexbuf }
-| "(*" { start_comment lexbuf; comment lexbuf }
-| '\n' { newline lexbuf; Buffer.add_char comment_buf '\n'; comment lexbuf }
-| (_ as c) { Buffer.add_char comment_buf c; comment lexbuf }
-| eof { lex_unexpected_eof lexbuf "comment" }
-
-and string = parse
-| '\"'
-  {
-    let s = Buffer.contents string_buf in
-    let () = Buffer.reset string_buf in
-    STRING s
-  }
-| "\\\"" { Buffer.add_char string_buf '\"'; string lexbuf }
-| '\n' { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
-| (_ as c) { Buffer.add_char string_buf c; string lexbuf }
-| eof { lex_unexpected_eof lexbuf "string" }
-
-and ocaml_string = parse
-| "\\\"" { Buffer.add_string ocaml_buf "\\\""; ocaml_string lexbuf }
-| '\"' { Buffer.add_char ocaml_buf '\"'; ocaml lexbuf }
-| (_ as c) { Buffer.add_char ocaml_buf c; ocaml_string lexbuf }
-| eof { lex_unexpected_eof lexbuf "OCaml string" }
-
-{
-
-let token lexbuf = match mode () with
-| OCaml -> ocaml lexbuf
-| Extend -> extend lexbuf
-
-}