From dd25b08c3608b55dd9edb24304168efb56bc64c8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 4 Jul 2018 16:48:01 +0200
Subject: [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.
---
 coqpp/coqpp_ast.mli | 95 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 95 insertions(+)
 create mode 100644 coqpp/coqpp_ast.mli

(limited to 'coqpp/coqpp_ast.mli')

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
new file mode 100644
index 000000000..39b4d2ab3
--- /dev/null
+++ b/coqpp/coqpp_ast.mli
@@ -0,0 +1,95 @@
+(************************************************************************)
+(*  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
-- 
cgit v1.2.3