From 87a81fd7e6ff6b45c76690471eb671ba4b005338 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Apr 2016 18:59:16 +0200
Subject: Moving and enhancing the grammar_tactic_prod_item_expr type.

---
 printing/ppvernac.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 9054ba0b67..f0548238a7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -104,12 +104,6 @@ module Make
     if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1))
     else id
 
-  let pr_production_item = function
-    | 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")"
-    | TacTerm s -> qs s
-
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
     | CommentString s -> qs s
-- 
cgit v1.2.3