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/extend.ml | 45 +++++++++++++--------------------------------
 1 file changed, 13 insertions(+), 32 deletions(-)

(limited to 'parsing/extend.ml')

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 9b85ada5..fca24ed5 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -1,42 +1,20 @@
 (************************************************************************)
 (*  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: extend.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
+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 =
@@ -45,21 +23,24 @@ type production_level =
 
 type ('lev,'pos) constr_entry_key_gen =
   | ETName | ETReference | ETBigint
-  | ETBinder of bool
+  | ETBinder of bool (* true=open, as in "fun .."; false as in "let f .. :=" *)
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
-  | ETConstrList of ('lev * 'pos) * Token.pattern list
-  | ETBinderList of bool * Token.pattern list
+  | ETConstrList of ('lev * 'pos) * Tok.t list
+  | ETBinderList of bool * 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
-- 
cgit v1.2.3