Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 34 insertions, 28 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index f4c98291..7643120f 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -6,52 +6,58 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
-(*i $Id: extend.ml 7761 2005-12-30 10:52:19Z herbelin $ i*)
+(*i $Id$ i*)
 
 open Util
-open Pp
-open Gramext
-open Names
-open Ppextend
-open Topconstr
-open Genarg
 
 (**********************************************************************)
-(* constr entry keys                                                  *)
+(* 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                                    *)
 
 type side = Left | Right
 
 type production_position =
-  | BorderProd of side * Gramext.g_assoc option  (* true=left; false=right *)
+  | BorderProd of side * Gramext.g_assoc option
   | InternalProd
 
 type production_level =
   | NextLevel
   | NumLevel of int
 
-type ('lev,'pos) constr_entry_key =
-  | ETIdent | ETReference | ETBigint
+type ('lev,'pos) constr_entry_key_gen =
+  | ETName | ETReference | ETBigint
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
   | ETConstrList of ('lev * 'pos) * Token.pattern list
 
-type constr_production_entry =
-    (production_level,production_position) constr_entry_key
-type constr_entry =
-    (int,unit) constr_entry_key
-type simple_constr_production_entry =
-    (production_level,unit) constr_entry_key
-
-(**********************************************************************)
-(* syntax modifiers                                                   *)
+(* Entries level (left-hand-side of grammar rules) *)
+type constr_entry_key =
+    (int,unit) constr_entry_key_gen
 
-type syntax_modifier =
-  | SetItemLevel of string list * production_level
-  | SetLevel of int
-  | SetAssoc of Gramext.g_assoc
-  | SetEntryType of string * simple_constr_production_entry
-  | SetOnlyParsing
-  | SetFormat of string located
+(* 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") *)
+type simple_constr_prod_entry_key =
+    (production_level,unit) constr_entry_key_gen