From 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 02:09:54 +0100
Subject: Moving Print Ltac 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 123b3ec1b7..1a67a37d7f 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -60,7 +60,6 @@ type printable =
   | PrintClasses
   | PrintTypeClasses
   | PrintInstances of reference or_by_notation
-  | PrintLtac of reference
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
   | PrintCanonicalConversions
-- 
cgit v1.2.3