Small fixes.

3 files changed, 16 insertions, 14 deletions

diff --git a/coq/coq-db.el b/coq/coq-db.el
index 65df920e..cf14c1cd 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -56,12 +56,12 @@ Explanation of the first line: the tactic menu entry mytac, abbreviated by mt,
 will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a
 new keyword to colorize." )
 
-(defun coq-insert-from-db (db)
+(defun coq-insert-from-db (db prompt)
   "Ask for a keyword, with completion on keyword database DB and insert.
 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 "tactic (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-syntax.el b/coq/coq-syntax.el
index e51fa16d..2775ac2d 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -36,6 +36,7 @@ none of these 2 variables is set to t, then ProofGeneral guesses the
 version of coq by doing 'coqtop -v'." )
 
 ;;FIXME: how to make compilable?
+;; post-cond: one of the variables is set to t
 (unless (noninteractive);; DA: evaluating here gives error during compile
   (let* 
       (
@@ -47,11 +48,10 @@ version of coq by doing 'coqtop -v'." )
                     " coq-version-is-V8-0 are set to true. This is"
                     "contradictory.")))
     (cond
-     ((and coq-version-is-V8-1 coq-version-is-V8-0) 
-      (error err))
+     ((and coq-version-is-V8-1 coq-version-is-V8-0) (error err))
      (coq-version-is-V8-1 (message v81))
      (coq-version-is-V8-0 (message v80))
-     (coq-version-is-V8 (setq coq-version-is-V8-0 t coq-version-is-V8-1 nil)
+     (coq-version-is-V8 (setq coq-version-is-V8-0 nil coq-version-is-V8-1 t)
                         (message v80))
      (t;; otherwise do coqtop -v and see which version we have
       (let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
diff --git a/coq/coq.el b/coq/coq.el
index 9af9b2f9..b0e3e2fb 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -149,7 +149,8 @@ To disable coqc being called (and use only make), set this to nil."
 (defconst coq-forget-id-command "Reset %s . ")
 (defconst coq-back-n-command "Back %s . ")
 
-
+;; some of them must kept when v8.1 because they are used by state preserving
+;; check when C-c C-v
 (defconst coq-state-preserving-tactics-regexp 
   (proof-ids-to-regexp coq-state-preserving-tactics))
 (defconst coq-state-changing-commands-regexp
@@ -568,13 +569,14 @@ If locked span already has a state number, thne do nothing. Also updates
 ;; when > 8.0: adapt
 (defun coq-find-and-forget (span)
   "Go back to SPAN.
-This function calls `coq-find-and-forget-v81' or
-`coq-find-and-forget-v80' depending on the variables `coq-version-is-V8-1' and
-`coq-version-is-V8-0', if none is set, then it default to `coq-find-and-forget-v80'."
+This function calls `coq-find-and-forget-v81' or `coq-find-and-forget-v80'
+depending on the variables `coq-version-is-V8-1' and `coq-version-is-V8-0', if
+none is set, then it default to `coq-find-and-forget-v81' but this should not
+happen since one of them is necessarily set to t in coq-syntax.el."
  (cond 
   (coq-version-is-V8-1 (coq-find-and-forget-v81 span))
   (coq-version-is-V8-0 (coq-find-and-forget-v80 span))
-  (t (coq-find-and-forget-v80 span)) ;; this is temporary
+  (t (coq-find-and-forget-v81 span)) ;; should not happen
   )
  )  
 
@@ -1337,25 +1339,25 @@ positions."
   "Ask for a tactic name, with completion on a quasi-exhaustive list of coq
 tactics and insert it at point.  Questions may be asked to the user."
   (interactive)
-  (coq-insert-from-db coq-tactics-db))
+  (coq-insert-from-db coq-tactics-db "Tactic"))
 
 (defun coq-insert-tactical ()
   "Ask for a tactical name, with completion on a quasi-exhaustive list of coq
 tacticals and insert it at point.  Questions may be asked to the user."
   (interactive)
-  (coq-insert-from-db coq-tacticals-db))
+  (coq-insert-from-db coq-tacticals-db "Tactical"))
 
 (defun coq-insert-command ()
   "Ask for a command name, with completion on a quasi-exhaustive list of coq
 commands and insert it at point.  Questions may be asked to the user."
   (interactive)
-  (coq-insert-from-db coq-commands-db))
+  (coq-insert-from-db coq-commands-db "Command"))
 
 (defun coq-insert-term ()
   "Ask for a term kind, with completion and insert it at point.  Questions may
 be asked to the user."
   (interactive)
-  (coq-insert-from-db coq-terms-db))
+  (coq-insert-from-db coq-terms-db "Kind of term"))
 
 
 (define-key coq-keymap [(control ?i)] 'coq-insert-intros)