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.
---
 printing/ppvernac.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4957199903..daba18bad2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -105,10 +105,9 @@ module Make
     else id
 
   let pr_production_item = function
-    | TacNonTerm (loc,nt,Some (p,sep)) ->
+    | TacNonTerm (loc, nt, (p, sep)) ->
       let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in
       str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
-    | TacNonTerm (loc,nt,None) -> str nt
     | TacTerm s -> qs s
 
   let pr_comment pr_c = function
-- 
cgit v1.2.3