Removing the Entry module now that rules need not be marshalled.

5 files changed, 1 insertions, 71 deletions

diff --git a/parsing/entry.ml b/parsing/entry.ml
deleted file mode 100644
index b7c6c23fa6..0000000000
--- a/parsing/entry.ml
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Errors
-open Util
-
-type 'a t = string
-
-(** Entries are registered with a unique name *)
-
-let entries = ref String.Set.empty
-
-let create name =
-  let () =
-    if String.Set.mem name !entries then
-    anomaly (Pp.str ("Entry " ^ name ^ " already defined"))
-  in
-  let () = entries := String.Set.add name !entries in
-  name
-
-let unsafe_of_name name =
-  assert (String.Set.mem name !entries);
-  name
-
-let repr s = s
diff --git a/parsing/entry.mli b/parsing/entry.mli
deleted file mode 100644
index 4c73fe2049..0000000000
--- a/parsing/entry.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Typed grammar entries *)
-
-type 'a t
-(** Typed grammar entries. We need to defined them here so that they are
-    marshallable and defined before the Pcoq.Gram module. They are basically
-    unique names. They should be kept synchronized with the {!Pcoq} entries. *)
-
-val create : string -> 'a t
-(** Create an entry. They should be synchronized with the entries defined in
-    {!Pcoq}. *)
-
-(** {5 Meta-programming} *)
-
-val repr : 'a t -> string
-val unsafe_of_name : string -> 'a t
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index b052b6ee6d..0e1c79c91b 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,7 +1,6 @@
 Tok
 Compat
 CLexer
-Entry
 Pcoq
 Egramml
 Egramcoq
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 70bcf1def3..a7f7ad7bca 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -215,18 +215,9 @@ let get_univ u =
 (** A table associating grammar to entries *)
 let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty
 
-let get_grammar (e : 'a Entry.t) : 'a Gram.entry =
-  Obj.magic (String.Map.find (Entry.repr e) !gtable)
-
-let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) =
-  assert (not (String.Map.mem (Entry.repr e) !gtable));
-  gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable
-
 let new_entry u s =
   let ename = u ^ ":" ^ s in
-  let entry = Entry.create ename in
   let e = Gram.entry_create ename in
-  let () = set_grammar entry e in
   e
 
 let make_gen_entry u s = new_entry u s
@@ -689,10 +680,8 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Aself -> Symbols.sself
   | Anext -> Symbols.snext
   | Aentry e ->
-    let e = get_grammar e in
     Symbols.snterm (Gram.Entry.obj (weaken_entry e))
   | Aentryl (e, n) ->
-    let e = get_grammar e in
     Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
   | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x))
 
@@ -726,8 +715,6 @@ let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   unsafe_grammar_extend e reinit ext
 
-let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
-
 let list_entry_names () = []
 
 let epsilon_value f e =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3723504149..70eb211067 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -19,7 +19,7 @@ open Genredexpr
 
 (** The parser of Coq *)
 
-module Gram : Compat.GrammarSig
+module Gram : module type of Compat.GrammarMake(CLexer)
 
 (** The parser of Coq is built from three kinds of rule declarations:
 
@@ -128,7 +128,6 @@ val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
-val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit
 val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
 val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
 
@@ -234,8 +233,6 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry
 val get_command_entry : unit -> vernac_expr Gram.entry
 val set_command_entry : vernac_expr Gram.entry -> unit
 
-val name_of_entry : 'a Gram.entry -> 'a Entry.t
-
 val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** Binding general entry keys to symbols *)