diff options
| -rw-r--r-- | coq/coq-system.el | 6 | ||||
| -rw-r--r-- | generic/proof-config.el | 6 | ||||
| -rw-r--r-- | generic/proof-menu.el | 2 | ||||
| -rw-r--r-- | generic/proof-site.el | 4 |
4 files changed, 9 insertions, 9 deletions
diff --git a/coq/coq-system.el b/coq/coq-system.el index 5b530e45..c090cecb 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -485,13 +485,13 @@ path (including the -R lib options) (see `coq-load-path')." (defcustom coq-project-filename "_CoqProject" "The name of coq project file. -The coq project file of a coq developpement (cf. Coq documentation on +The coq project file of a coq development (cf. Coq documentation on \"makefile generation\") should contain the arguments given to coq_makefile. In particular it contains the -I and -R options (preferably one per line). If `coq-use-coqproject' is -t (default) the content of this file will be used by proofgeneral to +t (default) the content of this file will be used by Proof General to infer the `coq-load-path' and the `coq-prog-args' variables that set -the coqtop invocation by proofgeneral. This is now the recommended +the coqtop invocation by Proof General. This is now the recommended way of configuring the coqtop invocation. Local file variables may still be used to override the coq project file's configuration. .dir-locals.el files also work and override project file settings." diff --git a/generic/proof-config.el b/generic/proof-config.el index 6f1e9148..8d5f9762 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -446,10 +446,10 @@ It's safe to leave this setting as nil." :group 'proof-script) (defcustom proof-goal-with-hole-result 2 - "How to get theorem name after ‘proof-goal-with-hole-regexp’ match. + "How to get theorem name after `proof-goal-with-hole-regexp' match. String or Int. -If an int N, use ‘match-string’ to get the value of the Nth parenthesis matched. -If a string, use ‘replace-match’. In this case, ‘proof-goal-with-hole-regexp’ +If an int N, use `match-string' to get the value of the Nth parenthesis matched. +If a string, use `replace-match'. In this case, `proof-goal-with-hole-regexp' should match the entire command." :type '(choice string integer) :group 'proof-script) diff --git a/generic/proof-menu.el b/generic/proof-menu.el index c17d4e95..c8c2239b 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -34,7 +34,7 @@ (defvar proof-display-some-buffers-count 0) (defun proof-display-some-buffers () - "Display the reponse, trace, goals, or shell buffer, rotating. + "Display the response, trace, goals, or shell buffer, rotating. A fixed number of repetitions of this command switches back to the same buffer. Also move point to the end of the response buffer if it's selected. diff --git a/generic/proof-site.el b/generic/proof-site.el index f47d8800..b149b7f1 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -125,7 +125,7 @@ (let ((s (getenv "PROOFGENERAL_HOME"))) (if s (file-name-as-directory s))))) "Directory where Proof General is installed. -based on where the file `proof-site.el' was loaded from. +Based on where the file `proof-site.el' was loaded from. Falls back to consulting the environment variable `PROOFGENERAL_HOME' if proof-site.el couldn't know where it was executed from.") @@ -204,7 +204,7 @@ assistant, `SYMBOL-mode', run when files with AUTOMODE-REGEXP \(or with extension FILE-EXTENSION) are visited. If present, IGNORED-EXTENSIONS-LIST is a list of file-name extensions to be ignored when doing file-name completion (IGNORED-EXTENSIONS-LIST -is added to ‘completion-ignored-extensions’). +is added to `completion-ignored-extensions'). SYMBOL is also used to form the name of the directory and elisp file for the mode, which will be |