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.

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

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 88bb805a72..edd32e8337 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -455,8 +455,6 @@ module Make
         keyword "Print TypeClasses"
       | PrintInstances qid ->
         keyword "Print Instances" ++ spc () ++ pr_smart_global qid
-      | PrintLtac qid ->
-        keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid
       | PrintCoercions ->
         keyword "Print Coercions"
       | PrintCoercionPaths (s,t) ->
-- 
cgit v1.2.3