From 624924d686c15ff3043aa579634aa07758dcca1b Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 9 Jul 2012 20:29:46 +0000 Subject: Fixed a small bug in indentation + added new commands for queries with Printing Implicit and Printing All flags. --- coq/coq-abbrev.el | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'coq/coq-abbrev.el') diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 538ad5ec..c279e91b 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -89,12 +89,18 @@ ("OTHER QUERIES" ["Print Hint" coq-PrintHint t] ["Show ith goal..." coq-Show t] + ["Show ith goal... (show implicits)" coq-Show-with-implicits t] + ["Show ith goal... (show all)" coq-Show-with-all t] ["Show Tree" coq-show-tree t] ["Show Proof" coq-show-proof t] ["Show Conjectures" coq-show-conjectures t];; maybe not so useful with editing in PG? "" ["Print..." coq-Print t] + ["Print... (show implicits)" coq-Print-with-implicits t] + ["Print... (show all)" coq-Print-with-all t] ["Check..." coq-Check t] + ["Check (show implicits)..." coq-Check-show-implicits t] + ["Check (show all)..." coq-Check-show-all t] ["About..." coq-About t] ["Search..." coq-SearchConstant t] ["SearchRewrite..." coq-SearchRewrite t] -- cgit v1.2.3