aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2009-10-15 17:16:37 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2009-10-15 17:16:37 +0000
commit9d16a972dc44dbb6d9035a9492e4f5c1135cedca (patch)
tree714ec9245e2aae0c0062cd06e13d8b62b92dbabb /coq
parenta578d6d624c2c9af0239ba7f06b93de7a4714f3c (diff)
Added keyboard shortcut in goals buffer.
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el13
1 files changed, 13 insertions, 0 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 8921ca82..d5f05ba5 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1207,6 +1207,19 @@ be asked to the user."
(define-key coq-keymap [(control ?n)] 'coq-LocateNotation)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?p)] 'coq-Print)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?o)] 'coq-SearchIsos)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?b)] 'coq-About)
+
+;
+;(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check)
+;(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?p)] 'coq-Print)
+;(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?o)] 'coq-SearchIsos)
+;(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?b)] 'coq-About)
+;
+
+
;;;;;;;;;;;;;;;;;;;;;;;;
;; error handling
;;;;;;;;;;;;;;;;;;;;;;;;