Use a homebrew parser to replace the GEXTEND extension points of Camlp5.

The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.

Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.

14 files changed, 791 insertions, 15 deletions

diff --git a/.gitignore b/.gitignore
index 6adbc9fb2..1eee3f94f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -115,6 +115,7 @@ dev/ocamldoc/*.css
 
 # .mll files
 
+grammar/coqpp_lex.ml
 dev/ocamlweb-doc/lex.ml
 ide/coq_lex.ml
 ide/config_lexer.ml
@@ -126,6 +127,11 @@ tools/ocamllibdep.ml
 tools/coqdoc/cpretty.ml
 ide/protocol/xml_lexer.ml
 
+# .mly files
+
+grammar/coqpp_parse.ml
+grammar/coqpp_parse.mli
+
 # .ml4 / .mlp files
 
 g_*.ml
diff --git a/Makefile b/Makefile
index 4787377ea..26d582c72 100644
--- a/Makefile
+++ b/Makefile
@@ -74,9 +74,11 @@ endef
 ## Files in the source tree
 
 LEXFILES := $(call find, '*.mll')
+YACCFILES := $(call find, '*.mly')
 export MLLIBFILES := $(call find, '*.mllib')
 export MLPACKFILES := $(call find, '*.mlpack')
 export ML4FILES := $(call find, '*.ml4')
+export MLGFILES := $(call find, '*.mlg')
 export CFILES := $(call findindir, 'kernel/byterun', '*.c')
 export MERLINFILES := $(call find, '.merlin')
 
@@ -90,7 +92,8 @@ EXISTINGMLI := $(call find, '*.mli')
 ## Files that will be generated
 
 GENML4FILES:= $(ML4FILES:.ml4=.ml)
-export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml
+GENMLGFILES:= $(MLGFILES:.mlg=.ml)
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
 
@@ -100,7 +103,7 @@ export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
 
 ## More complex file lists
 
-export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES), $(EXISTINGML))
+export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML))
 export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
 
 include Makefile.common
@@ -223,7 +226,7 @@ clean-ide:
 	rm -rf $(COQIDEAPP)
 
 ml4clean:
-	rm -f $(GENML4FILES)
+	rm -f $(GENML4FILES) $(GENMLGFILES)
 
 depclean:
 	find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -print | xargs rm -f
diff --git a/Makefile.build b/Makefile.build
index b85418243..884b73347 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -342,6 +342,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 GRAMBASEDEPS := grammar/q_util.cmi
 GRAMCMO := grammar/q_util.cmo \
  grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo
+COQPPCMO := grammar/coqpp_parse.cmo grammar/coqpp_lex.cmo
 
 grammar/argextend.cmo : $(GRAMBASEDEPS)
 grammar/q_util.cmo : $(GRAMBASEDEPS)
@@ -349,6 +350,10 @@ grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo
 grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \
  grammar/argextend.cmo
 
+grammar/coqpp_parse.cmi: grammar/coqpp_ast.cmi
+grammar/coqpp_parse.cmo: grammar/coqpp_ast.cmi grammar/coqpp_parse.cmi
+grammar/coqpp_lex.cmo: grammar/coqpp_ast.cmi grammar/coqpp_parse.cmo
+
 ## Ocaml compiler with the right options and -I for grammar
 
 GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
@@ -359,11 +364,15 @@ GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
 grammar/grammar.cma : $(GRAMCMO)
 	$(SHOW)'Testing $@'
 	@touch grammar/test.mlp
-	$(HIDE)$(GRAMC) -pp '$(CAMLP5O) -I $(MYCAMLP5LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test
+	$(HIDE)$(GRAMC) -pp '$(CAMLP5O) $^ -impl' -impl grammar/test.mlp -o grammar/test
 	@rm -f grammar/test.* grammar/test
 	$(SHOW)'OCAMLC -a $@'
 	$(HIDE)$(GRAMC) $^ -linkall -a -o $@
 
+grammar/coqpp: $(COQPPCMO) grammar/coqpp_main.ml
+	$(SHOW)'OCAMLC -a $@'
+	$(HIDE)$(GRAMC) $^ -linkall -o $@
+
 ## Support of Camlp5 and Camlp5
 
 COMPATCMO:=
@@ -376,6 +385,10 @@ grammar/%.cmo: grammar/%.mlp | $(COMPATCMO)
 	$(SHOW)'OCAMLC -c -pp $<'
 	$(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $<
 
+grammar/%.cmo: grammar/%.ml | $(COMPATCMO)
+	$(SHOW)'OCAMLC -c -pp $<'
+	$(HIDE)$(GRAMC) -c $<
+
 grammar/%.cmi: grammar/%.mli
 	$(SHOW)'OCAMLC -c $<'
 	$(HIDE)$(GRAMC) -c $<
@@ -746,11 +759,18 @@ plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLLEX  $<'
 	$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
 
-%.ml: %.ml4 $(CAMLP5DEPS)
+%.ml %.mli: %.mly
+	$(SHOW)'OCAMLYACC  $<'
+	$(HIDE)$(OCAMLYACC) --strict "$*.mly"
+
+%.ml: %.ml4 $(CAMLP5DEPS) grammar/coqpp
 	$(SHOW)'CAMLP5O   $<'
 	$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \
 	  $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@
 
+%.ml: %.mlg grammar/coqpp
+	$(SHOW)'COQPP   $<'
+	$(HIDE)grammar/coqpp $<
 
 ###########################################################################
 # Dependencies of ML code
diff --git a/configure.ml b/configure.ml
index b5d5a2419..c13c5e107 100644
--- a/configure.ml
+++ b/configure.ml
@@ -461,14 +461,19 @@ let _ = parse_args ()
 type camlexec =
  { mutable find : string;
    mutable top : string;
-   mutable lex : string; }
+   mutable lex : string;
+   mutable yacc : string;
+  }
 
 let camlexec =
   { find = "ocamlfind";
     top = "ocaml";
-    lex = "ocamllex"; }
+    lex = "ocamllex";
+    yacc = "ocamlyacc";
+  }
 
 let reset_caml_lex c o = c.lex <- o
+let reset_caml_yacc c o = c.yacc <- o
 let reset_caml_top c o = c.top <- o
 let reset_caml_find c o = c.find <- o
 
@@ -580,6 +585,9 @@ let camlbin, caml_version, camllib, findlib_version =
       if is_executable (camlbin / "ocamllex")
       then reset_caml_lex camlexec (camlbin / "ocamllex") in
     let () =
+      if is_executable (camlbin / "ocamlyacc")
+      then reset_caml_yacc camlexec (camlbin / "ocamlyacc") in
+    let () =
       if is_executable (camlbin / "ocaml")
       then reset_caml_top camlexec (camlbin / "ocaml") in
     camlbin, caml_version, camllib, findlib_version
@@ -1280,6 +1288,7 @@ let write_makefile f =
   pr "OCAML=%S\n" camlexec.top;
   pr "OCAMLFIND=%S\n" camlexec.find;
   pr "OCAMLLEX=%S\n" camlexec.lex;
+  pr "OCAMLYACC=%S\n" camlexec.yacc;
   pr "# The best compiler: native (=opt) or bytecode (=byte)\n";
   pr "BEST=%s\n\n" best_compiler;
   pr "# Ocaml version number\n";
diff --git a/grammar/coqpp_ast.mli b/grammar/coqpp_ast.mli
new file mode 100644
index 000000000..245e530ae
--- /dev/null
+++ b/grammar/coqpp_ast.mli
@@ -0,0 +1,80 @@
+(************************************************************************)
+(*  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 token_data =
+| TokNone
+| TokName of string
+| TokNameSep of string * string
+
+type ext_token =
+| ExtTerminal of string
+| ExtNonTerminal of string * 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 node =
+| Code of code
+| Comment of string
+| GramExt of grammar_ext
+| VernacExt
+| TacticExt of string * tactic_rule list
+
+type t = node list
diff --git a/grammar/coqpp_lex.mll b/grammar/coqpp_lex.mll
new file mode 100644
index 000000000..f35766b16
--- /dev/null
+++ b/grammar/coqpp_lex.mll
@@ -0,0 +1,163 @@
+(************************************************************************)
+(*  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']
+
+rule extend = parse
+| "(*" { start_comment (); comment lexbuf }
+| "{" { start_ocaml (); ocaml lexbuf }
+| "GRAMMAR" { GRAMMAR }
+| "VERNAC" { VERNAC }
+| "TACTIC" { TACTIC }
+| "EXTEND" { EXTEND }
+| "END" { END }
+(** 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) }
+| 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
new file mode 100644
index 000000000..23a5104e2
--- /dev/null
+++ b/grammar/coqpp_main.ml
@@ -0,0 +1,292 @@
+(************************************************************************)
+(*  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
+
+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 chan ext =
+  let locals = get_local_entries ext in
+  match locals with
+  | [] -> ()
+  | e :: locals ->
+    let mk_e chan e = fprintf chan "%s.Entry.create \"%s\"" ext.gramext_name e in
+    let () = fprintf chan "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in
+    let iter e = fprintf chan "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in
+    let () = List.iter iter locals in
+    fprintf chan "in@ "
+
+let print_string chan s = fprintf chan "\"%s\"" s
+
+let print_list chan pr l =
+  let rec prl chan = function
+  | [] -> ()
+  | [x] -> fprintf chan "%a" pr x
+  | x :: l -> fprintf chan "%a;@ %a" pr x prl l
+  in
+  fprintf chan "@[<hv>[%a]@]" prl l
+
+let print_opt chan pr = function
+| None -> fprintf chan "None"
+| Some x -> fprintf chan "Some@ (%a)" pr x
+
+let print_position chan pos = match pos with
+| First -> fprintf chan "Extend.First"
+| Last -> fprintf chan "Extend.Last"
+| Before s -> fprintf chan "Extend.Before@ \"%s\"" s
+| After s -> fprintf chan "Extend.After@ \"%s\"" s
+| Level s -> fprintf chan "Extend.Level@ \"%s\"" s
+
+let print_assoc chan = function
+| LeftA -> fprintf chan "Extend.LeftA"
+| RightA -> fprintf chan "Extend.RightA"
+| NonA -> fprintf chan "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 chan (vars, body) =
+  let vars = List.rev vars in
+  let iter = function
+  | None -> fprintf chan "_@ "
+  | Some id -> fprintf chan "%s@ " id
+  in
+  let () = fprintf chan "fun@ " in
+  let () = List.iter iter vars in
+  (** FIXME: use Coq locations in the macros *)
+  let () = fprintf chan "loc ->@ @[%s@]" body.code in
+  ()
+
+(** Meta-program instead of calling Tok.of_pattern here because otherwise
+    violates value restriction *)
+let print_tok chan = function
+| "", s -> fprintf chan "Tok.KEYWORD %a" print_string s
+| "IDENT", s -> fprintf chan "Tok.IDENT %a" print_string s
+| "PATTERNIDENT", s -> fprintf chan "Tok.PATTERNIDENT %a" print_string s
+| "FIELD", s -> fprintf chan "Tok.FIELD %a" print_string s
+| "INT", s -> fprintf chan "Tok.INT %a" print_string s
+| "STRING", s -> fprintf chan "Tok.STRING %a" print_string s
+| "LEFTQMARK", _ -> fprintf chan "Tok.LEFTQMARK"
+| "BULLET", s -> fprintf chan "Tok.BULLET %a" print_string s
+| "EOI", _ -> fprintf chan "Tok.EOI"
+| _ -> failwith "Tok.of_pattern: not a constructor"
+
+let rec print_prod chan 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 chan "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f
+
+and print_symbols chan = function
+| [] -> fprintf chan "Extend.Stop"
+| tkn :: tkns ->
+  fprintf chan "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn
+
+and print_symbol chan tkn = match tkn with
+| SymbToken (t, s) ->
+  let s = match s with None -> "" | Some s -> s in
+  fprintf chan "(Extend.Atoken (%a))" print_tok (t, s)
+| SymbEntry (e, None) ->
+  fprintf chan "(Extend.Aentry %s)" e
+| SymbEntry (e, Some l) ->
+  fprintf chan "(Extend.Aentryl (%s, %a))" e print_string l
+| SymbSelf ->
+  fprintf chan "Extend.Aself"
+| SymbNext ->
+  fprintf chan "Extend.Anext"
+| SymbList0 (s, None) ->
+  fprintf chan "(Extend.Alist0 %a)" print_symbol s
+| SymbList0 (s, Some sep) ->
+  fprintf chan "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep
+| SymbList1 (s, None) ->
+  fprintf chan "(Extend.Alist1 %a)" print_symbol s
+| SymbList1 (s, Some sep) ->
+  fprintf chan "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep
+| SymbOpt s ->
+  fprintf chan "(Extend.Aopt %a)" print_symbol s
+| SymbRules rules ->
+  let pr chan (r, body) =
+    let (vars, tkn) = List.split r in
+    let tkn = List.rev tkn in
+    fprintf chan "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body)
+  in
+  let pr chan rules = print_list chan pr rules in
+  fprintf chan "(Extend.Arules %a)" pr (List.rev rules)
+
+let print_rule chan r =
+  let pr_lvl chan lvl = print_opt chan print_string lvl in
+  let pr_asc chan asc = print_opt chan print_assoc asc in
+  let pr_prd chan prd = print_list chan print_prod prd in
+  fprintf chan "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods)
+
+let print_entry chan gram e =
+  let print_position_opt chan pos = print_opt chan print_position pos in
+  let print_rules chan rules = print_list chan print_rule rules in
+  fprintf chan "let () =@ @[%s.safe_extend@ %s@ @[(%a, %a)@]@]@ in@ "
+    gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
+
+let print_ast chan ext =
+  let () = fprintf chan "let _ = @[" in
+  let () = fprintf chan "@[<v>%a@]" print_local ext in
+  let () = List.iter (fun e -> print_entry chan ext.gramext_name e) ext.gramext_entries in
+  let () = fprintf chan "()@]\n" in
+  ()
+
+end
+
+let pr_ast chan = function
+| Code s -> fprintf chan "%s@\n" s.code
+| Comment s -> fprintf chan "%s@\n" s
+| GramExt gram -> fprintf chan "%a@\n" GramExt.print_ast gram
+| VernacExt -> fprintf chan "VERNACEXT@\n"
+| TacticExt (id, rules) ->
+  let pr_tok = function
+  | ExtTerminal s -> Printf.sprintf "%s" s
+  | ExtNonTerminal (s, _) -> Printf.sprintf "%s" s
+  in
+  let pr_tacrule r =
+    let toks = String.concat " " (List.map pr_tok r.tac_toks) in
+    Printf.sprintf "[%s] -> {%s}" toks r.tac_body.code
+  in
+  let rules = String.concat ", " (List.map pr_tacrule rules) in
+  fprintf chan "TACTICEXT (%s, [%s])@\n" id rules
+
+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
new file mode 100644
index 000000000..aa22d2717
--- /dev/null
+++ b/grammar/coqpp_parse.mly
@@ -0,0 +1,190 @@
+/************************************************************************/
+/*  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
+
+%}
+
+%token <Coqpp_ast.code> CODE
+%token <string> COMMENT
+%token <string> IDENT QUALID
+%token <string> STRING
+%token VERNAC TACTIC GRAMMAR EXTEND END
+%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 }
+| grammar_extend { $1 }
+| vernac_extend { $1 }
+| tactic_extend { $1 }
+;
+
+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_rules END { TacticExt ($3, $4)  }
+;
+
+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 { ExtNonTerminal ($1, TokNone) }
+| IDENT LPAREN IDENT RPAREN { ExtNonTerminal ($1, TokName $3) }
+| IDENT LPAREN IDENT COMMA STRING RPAREN { ExtNonTerminal ($1, TokNameSep ($3, $5)) }
+;
+
+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 }
+;
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 6cdd2ec19..0b8d7fda7 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -75,7 +75,7 @@ let rec mlexpr_of_prod_entry_key f = function
     (** Keep in sync with Pcoq! *)
     assert (e = "tactic");
     if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >>
-    else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >>
+    else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_string (string_of_int l)$ >>
 
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 6805a96ed..f57e32c88 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -101,7 +101,7 @@ type ('self, 'a) symbol =
 | Aself : ('self, 'self) symbol
 | Anext : ('self, 'self) symbol
 | Aentry : 'a entry -> ('self, 'a) symbol
-| Aentryl : 'a entry * int -> ('self, 'a) symbol
+| Aentryl : 'a entry * string -> ('self, 'a) symbol
 | Arules : 'a rules list -> ('self, 'a) symbol
 
 and ('self, _, 'r) rule =
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 6fdd9ea9b..171276a70 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -17,9 +17,17 @@ let curry f x y = f (x, y)
 let uncurry f (x,y) = f x y
 
 (** Location Utils  *)
+let ploc_file_of_coq_file = function
+| Loc.ToplevelInput -> ""
+| Loc.InFile f -> f
+
 let coq_file_of_ploc_file s =
   if s = "" then Loc.ToplevelInput else Loc.InFile s
 
+let of_coqloc loc =
+  let open Loc in
+  Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) ""
+
 let to_coqloc loc =
   { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
     Loc.line_nb = Ploc.line_nb loc;
@@ -236,7 +244,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Aentry e ->
     Symbols.snterm (G.Entry.obj e)
   | Aentryl (e, n) ->
-    Symbols.snterml (G.Entry.obj e, string_of_int n)
+    Symbols.snterml (G.Entry.obj e, n)
   | Arules rs ->
     G.srules' (List.map symbol_of_rules rs)
 
@@ -328,6 +336,7 @@ module Gram =
       I'm not entirely sure it makes sense, but at least it would be more correct.
           *)
       G.delete_rule e pil
+    let safe_extend e ext = grammar_extend e None ext
   end
 
 (** Remove extensions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f959bd80c..48604e188 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -80,6 +80,8 @@ module type S =
   (* Get comment parsing information from the Lexer *)
   val comment_state : coq_parsable -> ((int * int) * string) list
 
+  val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit
+
   (* Apparently not used *)
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
@@ -299,6 +301,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
 
 (** Location Utils  *)
+val of_coqloc : Loc.t -> Ploc.t
 val to_coqloc : Ploc.t -> Loc.t
 val (!@) : Ploc.t -> Loc.t
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 98d451536..876e6f320 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -45,7 +45,7 @@ let coincide s pat off =
 
 let atactic n =
   if n = 5 then Aentry Pltac.binder_tactic
-  else Aentryl (Pltac.tactic_expr, n)
+  else Aentryl (Pltac.tactic_expr, string_of_int n)
 
 type entry_name = EntryName :
   'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
@@ -398,7 +398,7 @@ let create_ltac_quotation name cast (e, l) =
   let () = ltac_quotations := String.Set.add name !ltac_quotations in
   let entry = match l with
   | None -> Aentry e
-  | Some l -> Aentryl (e, l)
+  | Some l -> Aentryl (e, string_of_int l)
   in
 (*   let level = Some "1" in *)
   let level = None in
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index cc9be7b0e..48f225f97 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -274,7 +274,7 @@ let make_sep_rules = function
   Arules [r]
 
 let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat ->
-  if is_binder_level from p then Aentryl (target_entry forpat, 200)
+  if is_binder_level from p then Aentryl (target_entry forpat, "200")
   else if is_self from p then Aself
   else
     let g = target_entry forpat in
@@ -282,7 +282,7 @@ let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p
     begin match lev with
     | None -> Aentry g
     | Some None -> Anext
-    | Some (Some (lev, cur)) -> Aentryl (g, lev)
+    | Some (Some (lev, cur)) -> Aentryl (g, string_of_int lev)
     end
 
 let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
@@ -291,7 +291,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
   Alist1 (symbol_of_target typ' assoc from forpat)
 | TTConstrList (typ', tkl, forpat) ->
   Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
-| TTPattern p -> Aentryl (Constr.pattern, p)
+| TTPattern p -> Aentryl (Constr.pattern, string_of_int p)
 | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
 | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
 | TTName -> Aentry Prim.name
@@ -428,6 +428,7 @@ let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
 let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with
 | Stop -> []
 | Next (rem, Aentryl (_, i)) ->
+  let i = int_of_string i in
   let rem = pure_sublevels level rem in
   begin match level with
   | Some j when Int.equal i j -> rem