diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-08-18 19:33:23 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-08-18 19:33:23 +0200 |
commit | 5f73b85cfcbb7cf0f39d212ce1d5a540e5b8ba22 (patch) | |
tree | a19ca0998160164a0af06c00cae1b0de13aaa030 /coq | |
parent | 37fa6de5424f62266593258d33cebad96d9d6d86 (diff) | |
parent | b7f17b7ca09276be5cd29263bd5574fdd6fa4d2c (diff) |
Merge branch 'master' of github.com:ProofGeneral/PG
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq.el | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -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) |