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.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index aef9b10b26..b8bc0483d3 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,Aentry (Entry.unsafe_of_name ("constr","constr")))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Pcoq.name_of_entry 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,Aentry (Entry.unsafe_of_name ("constr","constr")))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
-- 
cgit v1.2.3


From 805c8987fbb5fdeb94838bb5a3a7364c0a3d3374 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 17 Feb 2016 13:45:24 +0100
Subject: Do not export entry_key from Pcoq anymore.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b8bc0483d3..141eab3f3f 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,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
+        (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry 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,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
+        (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
-- 
cgit v1.2.3