From 4f52bd681ad9bbcbbd68406a58b47d8e962336ed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 20 Mar 2016 02:23:21 +0100
Subject: Moving the Ltac definition command to an EXTEND based command.

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

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 1a67a37d7..bd5890e29 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -379,7 +379,6 @@ type vernac_expr =
   | VernacBackTo of int
 
   (* Commands *)
-  | VernacDeclareTacticDefinition of tacdef_body list
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * reference list
   | VernacHints of obsolete_locality * string list * hints_expr
-- 
cgit v1.2.3