Fixes in strings/comments from Erik Martin-Dorel

4 files changed, 25 insertions, 30 deletions

diff --git a/coq/coq-db.el b/coq/coq-db.el
index 53ea970f..7fa7d1f4 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -72,7 +72,7 @@ new keyword to colorize.")
 Insert corresponding string with holes at point.  If an insertion function is
 present for the keyword, call it instead.  see `coq-syntax-db' for DB
 structure."
-  (let* ((tac (completing-read (concat prompt " (tab for completion) : ")
+  (let* ((tac (completing-read (concat prompt " (TAB for completion): ")
 			       db nil nil))
 	 (infos (cddr (assoc tac db)))
 	 (s (car infos)) ; completion to insert
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index e021909f..d860cabd 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -140,11 +140,11 @@ will be used to suggest values to the user."
       (setq olddirs (cdr olddirs)))
     ;; then ask for more
     (setq option (coq-read-directory
-                  "Add directory (tab to complete, empty to stop) -I:" ""))
+                  "Add directory (TAB to complete, empty to stop): -I " ""))
     (while (not (string-equal option ""))
       (setq progargs (cons option (cons "-I" progargs))) ;reversed
       (setq option (coq-read-directory
-                    "Add directory (tab to complete, empty to stop) -I :" "")))
+                    "Add directory (TAB to complete, empty to stop): -I " "")))
     (reverse progargs)))
 
 (defun coq-ask-prog-name (&optional oldvalue)
diff --git a/coq/coq.el b/coq/coq.el
index 181152e6..b489dd95 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -452,7 +452,7 @@ If locked span already has a state number, then do nothing. Also updates
   (interactive)
   (let*
       ((mods
-        (completing-read "Infos on notation (tab to see list): "
+        (completing-read "Infos on notation (TAB to see list): "
                          notation-print-kinds-table))
        (s (read-string  "Name (empty for all): "))
        (all (string-equal s "")))
@@ -514,12 +514,12 @@ This is specific to `coq-mode'."
 
 (defun coq-SearchRewrite ()
   (interactive)
-  (coq-ask-do "Search Rewrite" "SearchRewrite" nil))
+  (coq-ask-do "SearchRewrite" "SearchRewrite" nil))
 
 (defun coq-SearchAbout ()
   (interactive)
   (coq-ask-do 
-   "Search About (ex: \"eq_\" eq -bool)" 
+   "SearchAbout (ex: \"eq_\" eq -bool)" 
    "SearchAbout" nil 'coq-put-into-brackets))
 
 (defun coq-Print () 
@@ -538,20 +538,20 @@ This is specific to `coq-mode'."
   (coq-ask-do "Locate" "Locate"))
 
 (defun coq-LocateLibrary ()
-  "Locate a constant."
+  "Locate a library."
   (interactive)
   (coq-ask-do "Locate Library" "Locate Library"))
 
 (defun coq-LocateNotation ()
-  "Locate a notation.
+  "Locate a notation.  Put it automatically into quotes.
 This is specific to `coq-mode'."
   (interactive)
   (coq-ask-do 
-   "Locate Notation (ex: \'exists\' _ , _)" "Locate"
+   "Locate notation (ex: \'exists\' _ , _)" "Locate"
    t 'coq-put-into-quotes))
 
 (defun coq-Pwd ()
-  "Locate a notation."
+  "Display the current Coq working directory."
   (interactive)
   (proof-shell-invisible-command "Pwd."))
 
@@ -1052,11 +1052,11 @@ mouse activation."
   "Insert a module or a section after asking right questions."
   (interactive)
   (let*
-      ((mods (completing-read "kind of module (tab to see list): " module-kinds-table))
+      ((mods (completing-read "Kind of module (TAB to see list): " module-kinds-table))
        (s (read-string  "Name: "))
        (typkind (if (string-equal mods "Section")
                     "" ;; if not a section
-                  (completing-read "kind of type (optional, tab to see list): "
+                  (completing-read "Kind of type (optional, TAB to see list): "
                                    modtype-kinds-table)))
        (p (point)))
     (if (string-equal typkind "")
@@ -1079,7 +1079,7 @@ mouse activation."
   (let* ((s)
          (reqkind
           (completing-read 
-           "Command (tab to see list, default Require Export) : "
+           "Command (TAB to see list, default Require Export) : "
            reqkinds-kinds-table nil nil nil nil "Require Export")))
     (setq s (read-string  "Name (empty to stop) : "))
     (while (not (string-equal s ""))
@@ -1139,13 +1139,13 @@ Based on idea mentioned in Coq reference manual."
 
 
 (defun coq-insert-match ()
-  "Insert a match expression from a type name by Show Intros.
+  "Insert a match expression from a type name by Show Match.
 Based on idea mentioned in Coq reference manual. 
 Also insert holes at insertion positions."
   (interactive)
   (proof-shell-ready-prover)
   (let* ((cmd))
-    (setq cmd (read-string "Build match for type:"))
+    (setq cmd (read-string "Build match for type: "))
     (let* ((thematch
            (proof-shell-invisible-cmd-get-result (concat "Show Match " cmd ".")))
            (match (replace-regexp-in-string "=> \n" "=> #\n" thematch)))
diff --git a/generic/pg-user.el b/generic/pg-user.el
index ba255a67..ac04942a 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1251,19 +1251,14 @@ removed if it matches the last item in the ring."
 (defun pg-protected-undo (&optional arg)
   "As `undo' but avoids breaking the locked region.
 
-It performs a single undo/redo after checking that this operation
-will not affect the locked region.
-
-It performs each of the desired undos checking that these
-operations will not affect the locked region, obeying
-`proof-strict-read-only' if required.  If strict read only
-behaviour is enforced, the user is queried whether to 
-retract before the undo is allowed.  If automatic retraction is
-enabled, the retract and undo will go ahead without querying
-the user.
-
-Moreover, undo/redo is always allowed in comments 
-located in the locked region."
+It performs each of the desired undos checking that these operations will
+not affect the locked region, obeying `proof-strict-read-only' if required.
+If strict read only behaviour is enforced, the user is queried whether to
+retract before the undo is allowed.  If automatic retraction is enabled,
+the retract and undo will go ahead without querying the user.
+
+Moreover, undo/redo is always allowed in comments located in \
+the locked region."
   (interactive "*P")
   (if (or (not proof-locked-span)
   	  (equal (proof-queue-or-locked-end) (point-min)))
@@ -1275,7 +1270,7 @@ located in the locked region."
 	  (newarg ; Allow the user to limit the undo to the current region
 	   (and
 	    ;; this Boolean expression is necessary to match
-	    ;; the behavior of GNU Emacs undo function
+	    ;; the behavior of GNU Emacs (23.2) undo function
 	    (or (region-active-p) (and arg (not (numberp arg))))
 	    (> (region-end) (region-beginning)))))
       (while (> repeat 0)
@@ -1301,7 +1296,7 @@ behavior is expected."
 	   (end (max beg (- beg (cdr delta))))) ; Key computation
       (when (and next (> beg 0)		; the "next undo elt" exists
 		 (> (proof-queue-or-locked-end) beg)
-		 proof-strict-read-only ; edit freely doesn't undo
+		 proof-strict-read-only ; edit freely doesn't retract
 		 (not (and		; neither does edit in comments
 		       (proof-inside-comment beg) 
 		       (proof-inside-comment end))))