Do not export entry_key from Pcoq anymore.

4 files changed, 6 insertions, 31 deletions

diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 77252e7425..37fccdb3c2 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -9,6 +9,7 @@
 open Util
 open Compat
 open Names
+open Extend
 open Pcoq
 open Genarg
 open Vernacexpr
@@ -18,7 +19,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's grammar_prod_item
+      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index edf971574d..1ad9472007 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -16,7 +16,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
-      ('s, 'a) Pcoq.entry_key -> 's grammar_prod_item
+      ('s, 'a) Extend.symbol -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
   Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 238b9edd44..dac5b3bfd8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -64,21 +64,8 @@ let weaken_entry x = Gramobj.weaken_entry x
    dynamically interpreted as entries for the Coq level extensions
 *)
 
-type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
-| Atoken : Tok.t -> ('self, string) entry_key
-| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
-| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
-| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key
-| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Aself : ('self, 'self) entry_key
-| Anext : ('self, 'self) entry_key
-| Aentry : 'a Entry.t -> ('self, 'a) entry_key
-| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
-
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) entry_key -> entry_name
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) symbol -> entry_name
 
 (** Grammar extensions *)
 
@@ -684,7 +671,7 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
 
 (** Binding general entry keys to symbol *)
 
-let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
+let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Atoken t -> Symbols.stoken t
   | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
   | Alist1sep (s,sep) ->
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c1c0187137..d6bfe3eb39 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -112,19 +112,6 @@ type gram_reinit = gram_assoc * gram_position
    dynamically interpreted as entries for the Coq level extensions
 *)
 
-type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
-| Atoken : Tok.t -> ('self, string) entry_key
-| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
-| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
-| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key
-| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Aself : ('self, 'self) entry_key
-| Anext : ('self, 'self) entry_key
-| Aentry : 'a Entry.t -> ('self, 'a) entry_key
-| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
-
 (** Add one extension at some camlp4 position of some camlp4 entry *)
 val unsafe_grammar_extend :
   grammar_object Gram.entry ->
@@ -277,7 +264,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 (** Binding general entry keys to symbols *)
 
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (raw_tactic_expr, 'a) entry_key -> entry_name
+  'a raw_abstract_argument_type * (raw_tactic_expr, 'a) Extend.symbol -> entry_name
 
 (** [interp_entry_name lev n sep] returns the entry corresponding to the name
     [n] of the form "ne_constr_list" in a tactic entry of level [lev] with