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.

---
 toplevel/vernacentries.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index bdf0ada2cd..d0af1b951b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1582,7 +1582,6 @@ let vernac_print = function
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
-  | PrintLtac qid -> msg_notice (Tacintern.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> msg_notice (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
-- 
cgit v1.2.3