diff options
| -rw-r--r-- | coq/coq-syntax.el | 2 | ||||
| -rw-r--r-- | generic/proof.el | 11 |
2 files changed, 5 insertions, 8 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e351d905..65e63b60 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -28,7 +28,7 @@ ProofGeneral guesses the version of coq by doing 'coqtop -v'." ) (defvar coq-version-is-V8-1 nil "This variable can be set to t to force ProofGeneral to coq version coq-8.1 (use it for coq-8.0cvs after january 2005). To do that, put -(setq coq-version-is-V8-1 t) in your .emacs and restart emacs. This +\(setq coq-version-is-V8-1 t) in your .emacs and restart emacs. This variable cannot be true simultaneously with coq-version-is-V8-0. If none of these 2 variables is set to t, then ProofGeneral guesses the version of coq by doing 'coqtop -v'." ) diff --git a/generic/proof.el b/generic/proof.el index 6c93b7af..a3946c26 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -32,10 +32,10 @@ ;;; Global variables ;;; -(deflocal proof-buffer-type nil +(deflocal proof-buffer-type nil "Symbol for the type of this buffer: 'script, 'shell, 'goals, or 'response.") -(defvar proof-shell-busy nil +(defvar proof-shell-busy nil "A lock indicating that the proof shell is processing. When this is non-nil, proof-shell-ready-prover will give an error.") @@ -43,7 +43,7 @@ an error.") (defvar proof-included-files-list nil "List of files currently included in proof process. This list contains files in canonical truename format -(see `file-truename'). +\(see `file-truename'). Whenever a new file is being processed, it gets added to this list via the proof-shell-process-file configuration settings. @@ -106,12 +106,9 @@ of the proof (starting from 1).") ;; has been configured]. ;; We should assume commands are terminated at the specific level. -(defvar proof-terminal-string nil +(defvar proof-terminal-string nil "End-of-line string for proof process.") - - - ;;; ;;; Load other Proof General libraries ;;; |