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.

1 files changed, 3 insertions, 3 deletions

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)