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.

---
 tactics/g_ltac.ml4 | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'tactics')

diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4
index 3573ca7177..5c0ae215d8 100644
--- a/tactics/g_ltac.ml4
+++ b/tactics/g_ltac.ml4
@@ -404,3 +404,8 @@ VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF
     Metasyntax.add_tactic_notation (Locality.make_module_locality l, n, r, e)
   ]
 END
+
+VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
+| [ "Print" "Ltac" reference(r) ] ->
+  [ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
+END
-- 
cgit v1.2.3