aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-10-27 12:14:57 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-10-27 12:14:57 +0000
commit2c397c7f9b03f73a550456b8404b835486b3cff3 (patch)
tree83074a5b2f8e81ef4d52957aaf045ca9aef8eb4c /coq/coq.el
parent9a82ef99c0a9dac2aa988dbce358c10caef2d684 (diff)
Renamed proof-invisible-command proof-shell-invisible-command.
Removed superfluous optional 'relaxed' argument from: proof-shell-invisibile-command, proof-grab-lock, proof-start-queue.
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el5
1 files changed, 3 insertions, 2 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 106aa94d..73f58af9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -107,7 +107,7 @@
(remove-hook 'proof-shell-insert-hook 'coq-shell-init-hook))
(defun coq-set-undo-limit (undos)
- (proof-invisible-command (format "Set Undo %s." undos)))
+ (proof-shell-invisible-command (format "Set Undo %s." undos)))
(defun coq-count-undos (span)
(let ((ct 0) str i)
@@ -237,7 +237,8 @@
(let (cmd)
(proof-shell-ready-prover) ;; was (proof-check-process-available)
(setq cmd (read-string "Search Type: " nil 'proof-minibuffer-history))
- (proof-invisible-command (concat "Search " cmd proof-terminal-string))))
+ (proof-shell-invisible-command
+ (concat "Search " cmd proof-terminal-string))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Indentation ;;