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.

---
 intf/vernacexpr.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 14a80379ec..ae9328fcc0 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -200,10 +200,6 @@ type one_inductive_expr =
 type proof_expr =
   plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
 
-type grammar_tactic_prod_item_expr =
-  | TacTerm of string
-  | TacNonTerm of Loc.t * string * (Names.Id.t * string)
-
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
   | SetLevel of int
-- 
cgit v1.2.3