Fixes in strings/comments from Erik Martin-Dorel

3 files changed, 15 insertions, 15 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)))