Add (almost) compatibility with camlp4, without breaking support for camlp5

The choice between camlp4/5 is done during configure with flags
 -usecamlp5 (default for the moment) vs. -usecamlp4.

 Currently, to have a full camlp4 compatibility, you need to change
 all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
 into "`EOI" in grammar entries. I've a sed script that does that
 (actually the converse), but I prefer to re-think it and check a few
 things before branching this sed into the build mechanism.

 lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
 and try to propose a common interface (cf LexerSig / GrammarSig).
 A few incompatible quotations have been turned into underlying code
 manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
 parsable by both camlp4 and 5. See in particular the fate of
 <:str_item< declare ... end >>

 Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
 This forces to use camlp5 > 5.01.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 26 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index cc3551d32..4674a7c90 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -6,35 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Util
 
-(**********************************************************************)
-(* General entry keys *)
-
-(* This intermediate abstract representation of entries can           *)
-(* both be reified into mlexpr for the ML extensions and              *)
-(* dynamically interpreted as entries for the Coq level extensions    *)
-
-type 'a prod_entry_key =
-  | Alist1 of 'a prod_entry_key
-  | Alist1sep of 'a prod_entry_key * string
-  | Alist0 of 'a prod_entry_key
-  | Alist0sep of 'a prod_entry_key * string
-  | Aopt of 'a prod_entry_key
-  | Amodifiers of 'a prod_entry_key
-  | Aself
-  | Anext
-  | Atactic of int
-  | Agram of 'a Gramext.g_entry
-  | Aentry of string * string
-
-(**********************************************************************)
-(* Entry keys for constr notations                                    *)
+(** Entry keys for constr notations *)
 
 type side = Left | Right
 
 type production_position =
-  | BorderProd of side * Gramext.g_assoc option
+  | BorderProd of side * gram_assoc option
   | InternalProd
 
 type production_level =
@@ -48,14 +28,17 @@ type ('lev,'pos) constr_entry_key_gen =
   | ETOther of string * string
   | ETConstrList of ('lev * 'pos) * Tok.t list
 
-(* Entries level (left-hand-side of grammar rules) *)
+(**  Entries level (left-hand-side of grammar rules) *)
+
 type constr_entry_key =
     (int,unit) constr_entry_key_gen
 
-(* Entries used in productions (in right-hand-side of grammar rules) *)
+(** Entries used in productions (in right-hand-side of grammar rules) *)
+
 type constr_prod_entry_key =
     (production_level,production_position) constr_entry_key_gen
 
-(* Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+
 type simple_constr_prod_entry_key =
     (production_level,unit) constr_entry_key_gen