aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 13:40:16 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 13:40:16 +0000
commit91ce5d54ca9e53351e2bfcb7355fc890d9488da0 (patch)
tree5fccb82079d42dbc09c8f1c85aaad98871ca06df /coq
parent5205d2df95632ff2801ed416c0d3484ce6ec2e11 (diff)
pbp-mode -> goals-mode
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el13
1 files changed, 7 insertions, 6 deletions
diff --git a/coq/coq.el b/coq/coq.el
index a636a58f..408ffc76 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -15,7 +15,7 @@
(eval-and-compile
(mapcar (lambda (f) (autoload f "proof-shell"))
- '(pbp-mode proof-shell-config-done)))
+ '(proof-goals-mode proof-shell-config-done)))
; Configuration
@@ -115,9 +115,9 @@
(coq-mode-config)))
(eval-and-compile
- (define-derived-mode coq-pbp-mode pbp-mode
+ (define-derived-mode coq-goals-mode proof-goals-mode
"CoqGoals" nil
- (coq-pbp-mode-config)))
+ (coq-goals-mode-config)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Code that's coq specific ;;
@@ -397,8 +397,9 @@ This is specific to coq-mode."
(defun coq-pre-shell-start ()
(setq proof-prog-name coq-prog-name)
- (setq proof-mode-for-shell 'coq-shell-mode)
- (setq proof-mode-for-pbp 'coq-pbp-mode)
+ (setq proof-mode-for-shell 'coq-shell-mode)
+ (setq proof-mode-for-goals 'coq-goals-mode)
+ (setq proof-mode-for-response 'coq-response-mode)
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -526,7 +527,7 @@ This is specific to coq-mode."
(proof-shell-config-done))
-(defun coq-pbp-mode-config ()
+(defun coq-goals-mode-config ()
(setq pbp-change-goal "Show %s.")
(setq pbp-error-regexp coq-error-regexp)
(coq-init-syntax-table)