[coqpp] Move to its own directory.

Coqpp has nothing to do with `grammar`, we thus place it in its own
directory, which will prove convenient in more modular build systems.

Note that we add `coqpp` to the list of global includes, we could have
indeed added some extra rules, but IMHO not worth it as hopefully
proper containment will be soon checked by Dune.

4 files changed, 0 insertions, 867 deletions

diff --git a/grammar/coqpp_ast.mli b/grammar/coqpp_ast.mli
deleted file mode 100644
index 39b4d2ab3..000000000
--- a/grammar/coqpp_ast.mli
+++ /dev/null
@@ -1,95 +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        *)
-(************************************************************************)
-
-type loc = {
-  loc_start : Lexing.position;
-  loc_end : Lexing.position;
-}
-
-type code = { code : string }
-
-type user_symbol =
-| Ulist1 of user_symbol
-| Ulist1sep of user_symbol * string
-| Ulist0 of user_symbol
-| Ulist0sep of user_symbol * string
-| Uopt of user_symbol
-| Uentry of string
-| Uentryl of string * int
-
-type token_data =
-| TokNone
-| TokName of string
-
-type ext_token =
-| ExtTerminal of string
-| ExtNonTerminal of user_symbol * token_data
-
-type tactic_rule = {
-  tac_toks : ext_token list;
-  tac_body : code;
-}
-
-type level = string
-
-type position =
-| First
-| Last
-| Before of level
-| After of level
-| Level of level
-
-type assoc =
-| LeftA
-| RightA
-| NonA
-
-type gram_symbol =
-| GSymbString of string
-| GSymbQualid of string * level option
-| GSymbParen of gram_symbol list
-| GSymbProd of gram_prod list
-
-and gram_prod = {
-  gprod_symbs : (string option * gram_symbol list) list;
-  gprod_body : code;
-}
-
-type gram_rule = {
-  grule_label : string option;
-  grule_assoc : assoc option;
-  grule_prods : gram_prod list;
-}
-
-type grammar_entry = {
-  gentry_name : string;
-  gentry_pos : position option;
-  gentry_rules : gram_rule list;
-}
-
-type grammar_ext = {
-  gramext_name : string;
-  gramext_globals : string list;
-  gramext_entries : grammar_entry list;
-}
-
-type tactic_ext = {
-  tacext_name : string;
-  tacext_level : int option;
-  tacext_rules : tactic_rule list;
-}
-
-type node =
-| Code of code
-| Comment of string
-| DeclarePlugin of string
-| GramExt of grammar_ext
-| VernacExt
-| TacticExt of tactic_ext
-
-type t = node list
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
-
-}
diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml
deleted file mode 100644
index e76a1e9ed..000000000
--- a/grammar/coqpp_main.ml
+++ /dev/null
@@ -1,349 +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_ast
-open Format
-
-let fatal msg =
-  let () = Format.eprintf "Error: %s@\n%!" msg in
-  exit 1
-
-let pr_loc loc =
-  let file = loc.loc_start.pos_fname in
-  let line = loc.loc_start.pos_lnum in
-  let bpos = loc.loc_start.pos_cnum - loc.loc_start.pos_bol in
-  let epos = loc.loc_end.pos_cnum - loc.loc_start.pos_bol in
-  Printf.sprintf "File \"%s\", line %d, characters %d-%d:" file line bpos epos
-
-let parse_file f =
-  let chan = open_in f in
-  let lexbuf = Lexing.from_channel chan in
-  let () = lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = f } in
-  let ans =
-    try Coqpp_parse.file Coqpp_lex.token lexbuf
-    with
-    | Coqpp_lex.Lex_error (loc, msg) ->
-      let () = close_in chan in
-      let () = Printf.eprintf "%s\n%!" (pr_loc loc) in
-      fatal msg
-    | Parsing.Parse_error ->
-      let () = close_in chan in
-      let loc = Coqpp_lex.loc lexbuf in
-      let () = Printf.eprintf "%s\n%!" (pr_loc loc) in
-      fatal "syntax error"
-  in
-  let () = close_in chan in
-  ans
-
-module StringSet = Set.Make(String)
-
-let string_split s =
-  let len = String.length s in
-  let rec split n =
-    try
-      let pos = String.index_from s n '.' in
-      let dir = String.sub s n (pos-n) in
-      dir :: split (succ pos)
-    with
-      | Not_found -> [String.sub s n (len-n)]
-  in
-  if len == 0 then [] else split 0
-
-let plugin_name = "__coq_plugin_name"
-
-module GramExt :
-sig
-
-val print_ast : Format.formatter -> grammar_ext -> unit
-
-end =
-struct
-
-let is_uident s = match s.[0] with
-| 'A'..'Z' -> true
-| _ -> false
-
-let is_qualified = is_uident
-
-let get_local_entries ext =
-  let global = StringSet.of_list ext.gramext_globals in
-  let map e = e.gentry_name in
-  let entries = List.map map ext.gramext_entries in
-  let local = List.filter (fun e -> not (is_qualified e || StringSet.mem e global)) entries in
-  let rec uniquize seen = function
-  | [] -> []
-  | id :: rem ->
-    let rem = uniquize (StringSet.add id seen) rem in
-    if StringSet.mem id seen then rem else id :: rem
-  in
-  uniquize StringSet.empty local
-
-let print_local fmt ext =
-  let locals = get_local_entries ext in
-  match locals with
-  | [] -> ()
-  | e :: locals ->
-    let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in
-    let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in
-    let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in
-    let () = List.iter iter locals in
-    fprintf fmt "in@ "
-
-let print_string fmt s = fprintf fmt "\"%s\"" s
-
-let print_list fmt pr l =
-  let rec prl fmt = function
-  | [] -> ()
-  | [x] -> fprintf fmt "%a" pr x
-  | x :: l -> fprintf fmt "%a;@ %a" pr x prl l
-  in
-  fprintf fmt "@[<hv>[%a]@]" prl l
-
-let print_opt fmt pr = function
-| None -> fprintf fmt "None"
-| Some x -> fprintf fmt "Some@ (%a)" pr x
-
-let print_position fmt pos = match pos with
-| First -> fprintf fmt "Extend.First"
-| Last -> fprintf fmt "Extend.Last"
-| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s
-| After s -> fprintf fmt "Extend.After@ \"%s\"" s
-| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s
-
-let print_assoc fmt = function
-| LeftA -> fprintf fmt "Extend.LeftA"
-| RightA -> fprintf fmt "Extend.RightA"
-| NonA -> fprintf fmt "Extend.NonA"
-
-type symb =
-| SymbToken of string * string option
-| SymbEntry of string * string option
-| SymbSelf
-| SymbNext
-| SymbList0 of symb * symb option
-| SymbList1 of symb * symb option
-| SymbOpt of symb
-| SymbRules of ((string option * symb) list * code) list
-
-let is_token s = match string_split s with
-| [s] -> is_uident s
-| _ -> false
-
-let rec parse_tokens = function
-| [GSymbString s] -> SymbToken ("", Some s)
-| [GSymbQualid ("SELF", None)] -> SymbSelf
-| [GSymbQualid ("NEXT", None)] -> SymbNext
-| [GSymbQualid ("LIST0", None); tkn] ->
-  SymbList0 (parse_token tkn, None)
-| [GSymbQualid ("LIST1", None); tkn] ->
-  SymbList1 (parse_token tkn, None)
-| [GSymbQualid ("LIST0", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
-  SymbList0 (parse_token tkn, Some (parse_token tkn'))
-| [GSymbQualid ("LIST1", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
-  SymbList1 (parse_token tkn, Some (parse_token tkn'))
-| [GSymbQualid ("OPT", None); tkn] ->
-  SymbOpt (parse_token tkn)
-| [GSymbQualid (e, None)] when is_token e -> SymbToken (e, None)
-| [GSymbQualid (e, None); GSymbString s] when is_token e -> SymbToken (e, Some s)
-| [GSymbQualid (e, lvl)] when not (is_token e) -> SymbEntry (e, lvl)
-| [GSymbParen tkns] -> parse_tokens tkns
-| [GSymbProd prds] ->
-  let map p =
-    let map (pat, tkns) = (pat, parse_tokens tkns) in
-    (List.map map p.gprod_symbs, p.gprod_body)
-  in
-  SymbRules (List.map map prds)
-| t ->
-  let rec db_token = function
-  | GSymbString s -> Printf.sprintf "\"%s\"" s
-  | GSymbQualid (s, _) -> Printf.sprintf "%s" s
-  | GSymbParen s -> Printf.sprintf "(%s)" (db_tokens s)
-  | GSymbProd _ -> Printf.sprintf "[...]"
-  and db_tokens tkns =
-    let s = List.map db_token tkns in
-    String.concat " " s
-  in
-  fatal (Printf.sprintf "Invalid token: %s" (db_tokens t))
-
-and parse_token tkn = parse_tokens [tkn]
-
-let print_fun fmt (vars, body) =
-  let vars = List.rev vars in
-  let iter = function
-  | None -> fprintf fmt "_@ "
-  | Some id -> fprintf fmt "%s@ " id
-  in
-  let () = fprintf fmt "fun@ " in
-  let () = List.iter iter vars in
-  (** FIXME: use Coq locations in the macros *)
-  let () = fprintf fmt "loc ->@ @[%s@]" body.code in
-  ()
-
-(** Meta-program instead of calling Tok.of_pattern here because otherwise
-    violates value restriction *)
-let print_tok fmt = function
-| "", s -> fprintf fmt "Tok.KEYWORD %a" print_string s
-| "IDENT", s -> fprintf fmt "Tok.IDENT %a" print_string s
-| "PATTERNIDENT", s -> fprintf fmt "Tok.PATTERNIDENT %a" print_string s
-| "FIELD", s -> fprintf fmt "Tok.FIELD %a" print_string s
-| "INT", s -> fprintf fmt "Tok.INT %a" print_string s
-| "STRING", s -> fprintf fmt "Tok.STRING %a" print_string s
-| "LEFTQMARK", _ -> fprintf fmt "Tok.LEFTQMARK"
-| "BULLET", s -> fprintf fmt "Tok.BULLET %a" print_string s
-| "EOI", _ -> fprintf fmt "Tok.EOI"
-| _ -> failwith "Tok.of_pattern: not a constructor"
-
-let rec print_prod fmt p =
-  let (vars, tkns) = List.split p.gprod_symbs in
-  let f = (vars, p.gprod_body) in
-  let tkn = List.rev_map parse_tokens tkns in
-  fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f
-
-and print_symbols fmt = function
-| [] -> fprintf fmt "Extend.Stop"
-| tkn :: tkns ->
-  fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn
-
-and print_symbol fmt tkn = match tkn with
-| SymbToken (t, s) ->
-  let s = match s with None -> "" | Some s -> s in
-  fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s)
-| SymbEntry (e, None) ->
-  fprintf fmt "(Extend.Aentry %s)" e
-| SymbEntry (e, Some l) ->
-  fprintf fmt "(Extend.Aentryl (%s, %a))" e print_string l
-| SymbSelf ->
-  fprintf fmt "Extend.Aself"
-| SymbNext ->
-  fprintf fmt "Extend.Anext"
-| SymbList0 (s, None) ->
-  fprintf fmt "(Extend.Alist0 %a)" print_symbol s
-| SymbList0 (s, Some sep) ->
-  fprintf fmt "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep
-| SymbList1 (s, None) ->
-  fprintf fmt "(Extend.Alist1 %a)" print_symbol s
-| SymbList1 (s, Some sep) ->
-  fprintf fmt "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep
-| SymbOpt s ->
-  fprintf fmt "(Extend.Aopt %a)" print_symbol s
-| SymbRules rules ->
-  let pr fmt (r, body) =
-    let (vars, tkn) = List.split r in
-    let tkn = List.rev tkn in
-    fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body)
-  in
-  let pr fmt rules = print_list fmt pr rules in
-  fprintf fmt "(Extend.Arules %a)" pr (List.rev rules)
-
-let print_rule fmt r =
-  let pr_lvl fmt lvl = print_opt fmt print_string lvl in
-  let pr_asc fmt asc = print_opt fmt print_assoc asc in
-  let pr_prd fmt prd = print_list fmt print_prod prd in
-  fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods)
-
-let print_entry fmt gram e =
-  let print_position_opt fmt pos = print_opt fmt print_position pos in
-  let print_rules fmt rules = print_list fmt print_rule rules in
-  fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ "
-    gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
-
-let print_ast fmt ext =
-  let () = fprintf fmt "let _ = @[" in
-  let () = fprintf fmt "@[<v>%a@]" print_local ext in
-  let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in
-  let () = fprintf fmt "()@]@\n" in
-  ()
-
-end
-
-module TacticExt :
-sig
-
-val print_ast : Format.formatter -> tactic_ext -> unit
-
-end =
-struct
-
-let rec print_symbol fmt = function
-| Ulist1 s ->
-  fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s
-| Ulist1sep (s, sep) ->
-  fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep
-| Ulist0 s ->
-  fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s
-| Ulist0sep (s, sep) ->
-  fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep
-| Uopt s ->
-  fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s
-| Uentry e ->
-  fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e
-| Uentryl (e, l) ->
-  assert (e = "tactic");
-  fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
-
-let rec print_clause fmt = function
-| [] -> fprintf fmt "@[TyNil@]"
-| ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl
-| ExtNonTerminal (g, TokNone) :: cl ->
-  fprintf fmt "@[TyAnonArg (%a, %a)@]"
-    print_symbol g print_clause cl
-| ExtNonTerminal (g, TokName id) :: cl ->
-  fprintf fmt "@[TyArg (%a, \"%s\", %a)@]"
-    print_symbol g id print_clause cl
-
-let rec print_binders fmt = function
-| [] -> fprintf fmt "ist@ "
-| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders fmt rem
-| (ExtNonTerminal (_, TokName id)) :: rem ->
-  fprintf fmt "%s@ %a" id print_binders rem
-
-let print_rule fmt r =
-  fprintf fmt "@[TyML (%a, @[fun %a -> %s@])@]"
-    print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code
-
-let rec print_rules fmt = function
-| [] -> ()
-| [r] -> fprintf fmt "(%a)@\n" print_rule r
-| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem
-
-let print_rules fmt rules =
-  fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules
-
-let print_ast fmt ext =
-  let pr fmt () =
-    let level = match ext.tacext_level with None -> 0 | Some i -> i in
-    fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a"
-      plugin_name ext.tacext_name level print_rules ext.tacext_rules
-  in
-  let () = fprintf fmt "let () = @[%a@]\n" pr () in
-  ()
-
-end
-
-let pr_ast fmt = function
-| Code s -> fprintf fmt "%s@\n" s.code
-| Comment s -> fprintf fmt "%s@\n" s
-| DeclarePlugin name -> fprintf fmt "let %s = \"%s\"@\n" plugin_name name
-| GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram
-| VernacExt -> fprintf fmt "VERNACEXT@\n"
-| TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
-
-let () =
-  let () =
-    if Array.length Sys.argv <> 2 then fatal "Expected exactly one command line argument"
-  in
-  let file = Sys.argv.(1) in
-  let output = Filename.chop_extension file ^ ".ml" in
-  let ast = parse_file file in
-  let chan = open_out output in
-  let fmt = formatter_of_out_channel chan in
-  let iter ast = Format.fprintf fmt "@[%a@]%!"pr_ast ast in
-  let () = List.iter iter ast in
-  let () = close_out chan in
-  exit 0
diff --git a/grammar/coqpp_parse.mly b/grammar/coqpp_parse.mly
deleted file mode 100644
index baafd633c..000000000
--- a/grammar/coqpp_parse.mly
+++ /dev/null
@@ -1,256 +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 Coqpp_ast
-
-let starts s pat =
-  let len = String.length s in
-  let patlen = String.length pat in
-  if patlen <= len && String.sub s 0 patlen = pat then
-    Some (String.sub s patlen (len - patlen))
-  else None
-
-let ends s pat =
-  let len = String.length s in
-  let patlen = String.length pat in
-  if patlen <= len && String.sub s (len - patlen) patlen = pat then
-    Some (String.sub s 0 (len - patlen))
-  else None
-
-let between s pat1 pat2 = match starts s pat1 with
-| None -> None
-| Some s -> ends s pat2  
-
-let without_sep k sep r =
-  if sep <> "" then raise Parsing.Parse_error else k r
-
-let parse_user_entry s sep =
-  let table = [
-    "ne_", "_list", without_sep (fun r -> Ulist1 r);
-    "ne_", "_list_sep", (fun sep r -> Ulist1sep (r, sep));
-    "", "_list", without_sep (fun r -> Ulist0 r);
-    "", "_list_sep", (fun sep r -> Ulist0sep (r, sep));
-    "", "_opt", without_sep (fun r -> Uopt r);
-  ] in
-  let rec parse s sep = function
-  | [] ->
-    let () = without_sep ignore sep () in
-    begin match starts s "tactic" with
-    | Some ("0"|"1"|"2"|"3"|"4"|"5") -> Uentryl ("tactic", int_of_string s)
-    | Some _ | None -> Uentry s
-    end
-  | (pat1, pat2, k) :: rem ->
-    match between s pat1 pat2 with
-    | None -> parse s sep rem
-    | Some s ->
-      let r = parse s "" table in
-      k sep r      
-  in
-  parse s sep table
-
-%}
-
-%token <Coqpp_ast.code> CODE
-%token <string> COMMENT
-%token <string> IDENT QUALID
-%token <string> STRING
-%token <int> INT
-%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN
-%token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL
-%token LPAREN RPAREN COLON SEMICOLON
-%token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
-%token EOF
-
-%type <Coqpp_ast.t> file
-%start file
-
-%%
-
-file:
-| nodes EOF
-  { $1 }
-;
-
-nodes:
-|
-  { [] }
-| node nodes
-  { $1 :: $2 }
-;
-
-node:
-| CODE { Code $1 }
-| COMMENT { Comment $1 }
-| declare_plugin { $1 }
-| grammar_extend { $1 }
-| vernac_extend { $1 }
-| tactic_extend { $1 }
-;
-
-declare_plugin:
-| DECLARE PLUGIN STRING { DeclarePlugin $3 }
-;
-
-grammar_extend:
-| GRAMMAR EXTEND qualid_or_ident globals gram_entries END
-  { GramExt { gramext_name = $3; gramext_globals = $4; gramext_entries = $5 } }
-;
-
-vernac_extend:
-| VERNAC EXTEND IDENT END { VernacExt }
-;
-
-tactic_extend:
-| TACTIC EXTEND IDENT tactic_level tactic_rules END
-  { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } }
-;
-
-tactic_level:
-| { None }
-| LEVEL INT { Some $2 }
-;
-
-tactic_rules:
-| tactic_rule { [$1] }
-| tactic_rule tactic_rules { $1 :: $2 }
-;
-
-tactic_rule:
-| PIPE LBRACKET ext_tokens RBRACKET ARROW CODE
-  { { tac_toks = $3; tac_body = $6 } }
-;
-
-ext_tokens:
-| { [] }
-| ext_token ext_tokens { $1 :: $2 }
-;
-
-ext_token:
-| STRING { ExtTerminal $1 }
-| IDENT {
-  let e = parse_user_entry $1 "" in
-  ExtNonTerminal (e, TokNone) 
-  }
-| IDENT LPAREN IDENT RPAREN {
-  let e = parse_user_entry $1 "" in
-  ExtNonTerminal (e, TokName $3)
-  }
-| IDENT LPAREN IDENT COMMA STRING RPAREN {
-  let e = parse_user_entry $1 $5 in
-  ExtNonTerminal (e, TokName $3)
-}
-;
-
-qualid_or_ident:
-| QUALID { $1 }
-| IDENT { $1 }
-;
-
-globals:
-| { [] }
-| GLOBAL COLON idents SEMICOLON { $3 }
-;
-
-idents:
-| { [] }
-| qualid_or_ident idents { $1 :: $2 }
-;
-
-gram_entries:
-| { [] }
-| gram_entry gram_entries { $1 :: $2 }
-;
-
-gram_entry:
-| qualid_or_ident COLON position_opt LBRACKET levels RBRACKET SEMICOLON
-  { { gentry_name = $1; gentry_pos = $3; gentry_rules = $5; } }
-;
-
-position_opt:
-| { None }
-| position { Some $1 }
-;
-
-position:
-| FIRST { First }
-| LAST { Last }
-| BEFORE STRING { Before $2 }
-| AFTER STRING { After $2 }
-| LEVEL STRING { Level $2 }
-;
-
-string_opt:
-| { None }
-| STRING { Some $1 }
-;
-
-assoc_opt:
-| { None }
-| assoc { Some $1 }
-;
-
-assoc:
-| LEFTA { LeftA }
-| RIGHTA { RightA }
-| NONA { NonA }
-;
-
-levels:
-| level { [$1] }
-| level PIPE levels { $1 :: $3 }
-;
-
-level:
-| string_opt assoc_opt LBRACKET rules_opt RBRACKET
-  { { grule_label = $1; grule_assoc = $2; grule_prods = $4; } }
-;
-
-rules_opt:
-| { [] }
-| rules { $1 }
-;
-
-rules:
-| rule { [$1] }
-| rule PIPE rules { $1 :: $3 }
-;
-
-rule:
-| symbols_opt ARROW CODE
-  { { gprod_symbs = $1; gprod_body = $3; } }
-;
-
-symbols_opt:
-| { [] }
-| symbols { $1 }
-;
-
-symbols:
-| symbol { [$1] }
-| symbol SEMICOLON symbols { $1 :: $3 }
-;
-
-symbol:
-| IDENT EQUAL gram_tokens { (Some $1, $3) }
-| gram_tokens { (None, $1) }
-;
-
-gram_token:
-| qualid_or_ident { GSymbQualid ($1, None) }
-| qualid_or_ident LEVEL STRING { GSymbQualid ($1, Some $3) }
-| LPAREN gram_tokens RPAREN { GSymbParen $2 }
-| LBRACKET rules RBRACKET { GSymbProd $2 }
-| STRING { GSymbString $1 }
-;
-
-gram_tokens:
-| gram_token { [$1] }
-| gram_token gram_tokens { $1 :: $2 }
-;