From a252293101320b641365619b8d8a3ee914b781f4 Mon Sep 17 00:00:00 2001
From: John Grosen <jmgrosen@gmail.com>
Date: Tue, 7 Aug 2018 14:33:40 -0400
Subject: Add coq-Print-Ltac to print an Ltac term

---
 coq/coq.el | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/coq/coq.el b/coq/coq.el
index d3009696..96a9bf41 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1066,6 +1066,11 @@ With flag Printing All if some prefix arg is given (C-u)."
       (coq-ask-do-show-all "Print" "Print")
     (coq-ask-do "Print" "Print")))
 
+(defun coq-Print-Ltac ()
+  "Ask for an ident and print the corresponding Ltac term."
+  (interactive)
+  (coq-ask-do "Print Ltac" "Print Ltac"))
+
 (defun coq-Print-with-implicits ()
   "Ask for an ident and print the corresponding term."
   (interactive)
-- 
cgit v1.2.3