diff options
| author |  Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1997-10-30 15:58:33 +0000 |
|---|---|---|
| committer | Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1997-10-30 15:58:33 +0000 |
| commit | dbaa145b6a390b2febaf0cff7b3a759d6589d819 (patch) | |
| tree | 63f9675325bf3ccb1661554f25f261dcfe45d0e9 /proof.el | |
| parent | 88c3310c6dcde027d1e70d7a0cbf711f6972d842 (diff) | |
Updates for coq, including:
* pbp-goal-command and pbp-hyp-command use proof-terminal-string
* updates to keywords
* fix for goal regexp
Diffstat (limited to 'proof.el')
| -rw-r--r-- | proof.el | 14 |
1 files changed, 11 insertions, 3 deletions
@@ -19,6 +19,12 @@ ;; report ;; $Log$ +;; Revision 1.19 1997/10/30 15:58:33 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; ;; Revision 1.18 1997/10/24 14:51:13 hhg ;; Updated comment about extent types ;; @@ -484,12 +490,11 @@ ;; Proof by pointing ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconst pbp-goal-command "Pbp %s;" +(defvar pbp-goal-command nil "Command informing the prover that `pbp-button-action' has been requested on a goal.") - -(defconst pbp-hyp-command "PbpHyp %s;" +(defvar pbp-hyp-command nil "Command informing the prover that `pbp-button-action' has been requested on an assumption.") @@ -1197,6 +1202,9 @@ current command." (setq proof-terminal-string (char-to-string proof-terminal-char)) + (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) + (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) + (make-local-variable 'comment-start) (setq comment-start (concat proof-comment-start " ")) (make-local-variable 'comment-end) |