From 5b6582f8d47975f6f4f394cf44a1c65c799d43ff Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 4 Oct 2012 11:53:07 +0000
Subject: Moved Compat to parsing. This permits to break the dependency of the
 kernel on CAMLP4/5 structures, and consequently should also erase such
 structures from vo files.

This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 intf/extend.mli     | 11 ++++++++++-
 intf/vernacexpr.mli |  2 +-
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/extend.mli b/intf/extend.mli
index ca40eb7443..d66f29ba72 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -10,8 +10,17 @@
 
 type side = Left | Right
 
+type gram_assoc = NonA | RightA | LeftA
+
+type gram_position =
+  | First
+  | Last
+  | Before of string
+  | After of string
+  | Level of string
+
 type production_position =
-  | BorderProd of side * Compat.gram_assoc option
+  | BorderProd of side * gram_assoc option
   | InternalProd
 
 type production_level =
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index dfa03a4d75..31c1643d24 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -185,7 +185,7 @@ type grammar_tactic_prod_item_expr =
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
   | SetLevel of int
-  | SetAssoc of Compat.gram_assoc
+  | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing of Flags.compat_version
   | SetFormat of string located
-- 
cgit v1.2.3