From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 parsing/egrammar.mli | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

(limited to 'parsing/egrammar.mli')

diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 8554c9be..1d85c74e 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: egrammar.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
+open Compat
 open Util
 open Names
 open Topconstr
@@ -16,36 +14,35 @@ open Pcoq
 open Extend
 open Vernacexpr
 open Ppextend
-open Rawterm
+open Glob_term
 open Genarg
 open Mod_subst
-(*i*)
 
 (** Mapping of grammar productions to camlp4 actions
     Used for Coq-level Notation and Tactic Notation,
     and for ML-level tactic and vernac extensions
  *)
 
-(* For constr notations *)
+(** For constr notations *)
 
 type grammar_constr_prod_item =
-  | GramConstrTerminal of Token.pattern
+  | GramConstrTerminal of Tok.t
   | 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
+    int * gram_assoc option * notation * grammar_constr_prod_item list list
 
-(* For tactic and vernac notations *)
+(** For tactic and vernac notations *)
 
 type grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal of loc * argument_type *
-      Gram.te prod_entry_key * identifier option
+      prod_entry_key * identifier option
 
-(* Adding notations *)
+(** Adding notations *)
 
 type all_grammar_command =
   | Notation of
@@ -64,7 +61,7 @@ val extend_tactic_grammar :
   string -> grammar_prod_item list list -> unit
 
 val extend_vernac_command_grammar :
-  string -> grammar_prod_item list list -> unit
+  string -> vernac_expr Gram.entry option -> grammar_prod_item list list -> unit
 
 val get_extend_vernac_grammars :
  unit -> (string * grammar_prod_item list list) list
-- 
cgit v1.2.3