- Cleaning (unification of ML names, removal of obsolete code,

  reorganization of code) and documentation (in pcoq.mli) of the code
  for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
  Notation, Notation); merged the two copies of interp_entry_name to
  avoid they diverge.  
- Added support in Tactic Notation for ne_..._list_sep in general and
  for (ne_)ident_list(_sep) in particular.



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

1 files changed, 29 insertions, 28 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 36e1000b1..2121671a8 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -6,52 +6,53 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
 (*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 =
+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                                                   *)
-
-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
-
+type constr_prod_entry_key =
+    (production_level,production_position) constr_entry_key_gen
+type constr_entry_key =
+    (int,unit) constr_entry_key_gen
+type simple_constr_prod_entry_key =
+    (production_level,unit) constr_entry_key_gen