From a5e1b40b93e47a278746ee6752474891cd856c29 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 31 Dec 2015 19:26:02 +0100
Subject: Simplification of grammar_prod_item type.

Actually the identifier was never used and just carried along.
---
 dev/top_printers.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0894e0378d..cbebcdfcd4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,8 +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")),
-	 Some (Names.Id.of_string "c"))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
 
 let _ =
   try
@@ -537,8 +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")),
-	 Some (Names.Id.of_string "c"))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
 
 (* Setting printer of unbound global reference *)
 open Names
-- 
cgit v1.2.3