diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2012-07-09 20:29:46 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2012-07-09 20:29:46 +0000 |
| commit | 624924d686c15ff3043aa579634aa07758dcca1b (patch) | |
| tree | 6bfdbaceac744ead5e621b493248c66b369767dc /coq/coq-abbrev.el | |
| parent | e128ab922bf80e2158783d6ea43c18b9c48e84f1 (diff) | |
Fixed a small bug in indentation + added new commands for queries with
Printing Implicit and Printing All flags.
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 6 |
1 files changed, 6 insertions, 0 deletions
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] |