From 6150d15647afc739329019f7e9de595187ecc282 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 16:08:50 +0200
Subject: Removing the Entry module now that rules need not be marshalled.

---
 parsing/entry.mli | 23 -----------------------
 1 file changed, 23 deletions(-)
 delete mode 100644 parsing/entry.mli

(limited to 'parsing/entry.mli')

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
-- 
cgit v1.2.3