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.

---
 dev/printers.mllib  | 1 -
 dev/top_printers.ml | 4 ++--
 2 files changed, 2 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 390a9f384d..aa74cb5085 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -194,7 +194,6 @@ Proof_global
 Pfedit
 Decl_mode
 Ppconstr
-Entry
 Pcoq
 Printer
 Pptactic
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9c1971a82..f5599d793f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,7 +520,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
+        (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
 
 let _ =
   try
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
+        (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
 
 (* Setting printer of unbound global reference *)
 open Names
-- 
cgit v1.2.3