From a99aa093b962e228817066d00f7e12698f8df73a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Mar 2016 22:27:17 +0100
Subject: Simplifying the code of Entry.

---
 parsing/entry.mli | 29 ++++-------------------------
 1 file changed, 4 insertions(+), 25 deletions(-)

(limited to 'parsing/entry.mli')

diff --git a/parsing/entry.mli b/parsing/entry.mli
index 97cd5b1105..4c73fe2049 100644
--- a/parsing/entry.mli
+++ b/parsing/entry.mli
@@ -11,34 +11,13 @@
 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 made of a universe and an entry name. They should be kept
-    synchronized with the {!Pcoq} entries though. *)
+    unique names. They should be kept synchronized with the {!Pcoq} entries. *)
 
-type repr = string * string
-(** Representation of entries. *)
-
-(** Table of Coq statically defined grammar entries *)
-
-type universe
-
-(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
-
-val get_univ : string -> universe
-val univ_name : universe -> string
-
-val uprim : universe
-val uconstr : universe
-val utactic : universe
-val uvernac : universe
-
-(** {5 Uniquely defined entries} *)
-
-val create : universe -> string -> 'a t
+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 -> repr
-
-val unsafe_of_name : (string * string) -> 'a t
+val repr : 'a t -> string
+val unsafe_of_name : string -> 'a t
-- 
cgit v1.2.3