Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 29 insertions, 28 deletions

diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index d2d912d1..1228b40c 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -6,62 +6,63 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: egrammar.mli 10122 2007-09-15 10:35:59Z letouzey $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
+open Names
 open Topconstr
 open Pcoq
 open Extend
 open Vernacexpr
 open Ppextend
 open Rawterm
+open Genarg
 open Mod_subst
 (*i*)
 
 (** Mapping of grammar productions to camlp4 actions
-    Used for Coq-level Notation and Tactic Notation, 
+    Used for Coq-level Notation and Tactic Notation,
     and for ML-level tactic and vernac extensions
  *)
 
-type prod_item =
-  | Term of Token.pattern
-  | NonTerm of constr_production_entry * 
-      (Names.identifier * constr_production_entry) option
+(* For constr notations *)
 
-type notation_grammar = 
-    int * Gramext.g_assoc option * notation * prod_item list
+type grammar_constr_prod_item =
+  | GramConstrTerminal of Token.pattern
+  | GramConstrNonTerminal of constr_prod_entry_key * identifier option
+  | GramConstrListMark of int * bool
+    (* tells action rule to make a list of the n previous parsed items; 
+       concat with last parsed list if true *)
+
+type notation_grammar =
+    int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list
+
+(* For tactic and vernac notations *)
+
+type grammar_prod_item =
+  | GramTerminal of string
+  | GramNonTerminal of loc * argument_type *
+      Gram.te prod_entry_key * identifier option
+
+(* Adding notations *)
 
 type all_grammar_command =
   | Notation of (precedence * tolerability list) * notation_grammar
   | TacticGrammar of
-      (string * int * grammar_production list * 
-        (Names.dir_path * Tacexpr.glob_tactic_expr))
+      (string * int * grammar_prod_item list *
+         (dir_path * Tacexpr.glob_tactic_expr))
 
 val extend_grammar : all_grammar_command -> unit
 
-(* Add grammar rules for tactics *)
-
-type grammar_tactic_production =
-  | TacTerm of string
-  | TacNonTerm of
-      loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option
-
 val extend_tactic_grammar :
-  string -> grammar_tactic_production list list -> unit
+  string -> grammar_prod_item list list -> unit
 
 val extend_vernac_command_grammar :
-  string -> grammar_tactic_production list list -> unit
-(*
-val get_extend_tactic_grammars :
- unit -> (string * grammar_tactic_production list list) list
-*)
+  string -> grammar_prod_item list list -> unit
+
 val get_extend_vernac_grammars :
- unit -> (string * grammar_tactic_production list list) list
-(*
-val reset_extend_grammars_v8 : unit -> unit
-*)
-val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol
+ unit -> (string * grammar_prod_item list list) list
 
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) -> notation_grammar