fix typos and unicode single quotations in doc strings

Backported those typos that were fixed only in the manual texi
sources and not in the doc strings, from which the text was
imported. Convert a few symbols quoted with curved unicode single
quotations to ascii, such that make magic recognizes them.

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