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.

1 files changed, 80 insertions, 0 deletions

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