From a252293101320b641365619b8d8a3ee914b781f4 Mon Sep 17 00:00:00 2001 From: John Grosen 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 From 0d7a62f36b532dffa5fe8e55e6b1a1775e6c17e6 Mon Sep 17 00:00:00 2001 From: Javier Date: Wed, 15 Aug 2018 17:00:32 +0800 Subject: Update INSTALL --- INSTALL | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/INSTALL b/INSTALL index 31331c2f..3b496bd7 100644 --- a/INSTALL +++ b/INSTALL @@ -57,7 +57,7 @@ Detailed installation Notes for Proof General Supported Emacs Versions. ------------------------- -Please see COMPATIBILTY. +Please see COMPATIBILITY. If you're not sure of your version of Emacs, inspect the variable `emacs-version' by doing: -- cgit v1.2.3