Added something in the doc about coq-version-is-V7, and made the setting of

this variable more trustable with (concat coq-prog-name "-v").

1 files changed, 11 insertions, 8 deletions

diff --git a/coq/coq.el b/coq/coq.el
index be65c1cd..87122623 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -18,14 +18,6 @@
 	  "/usr/local/lib/coq"
       c)))
 
-;;Pierre: we will have both versions V6 and V7 during a while
-;;        the test with "coqtop -v" can be skipped if the variable 
-;;        coq-version-is-V7 is already set (usefull for people 
-;;        dealing with several version of coq)
-(if (boundp 'coq-version-is-V7) () ; if this variable is bound, do nothing 
-  (setq coq-version-is-V7          ; else test with "coqtop -v"
-	(if (string-match "version 7" (shell-command-to-string "coqtop -v")) 
-	    t nil)))
 
 (defcustom coq-tags (concat (coq-library-directory) "/theories/TAGS")
   "the default TAGS table for the Coq library"
@@ -75,6 +67,17 @@
 (defconst coq-shell-init-cmd 
   (format "Set Undo %s." coq-default-undo-limit))
 
+
+;;Pierre: we will have both versions V6 and V7 during a while
+;;        the test with "coqtop -v" can be skipped if the variable 
+;;        coq-version-is-V7 is already set (usefull for people 
+;;        dealing with several version of coq)
+(if (boundp 'coq-version-is-V7) () ; if this variable is bound, do nothing 
+  (setq coq-version-is-V7          ; else test with "coqtop -v"
+	(if (string-match "version 7" (shell-command-to-string (concat coq-prog-name " -v"))) 
+	    (progn (message "coq is V7") t)
+	  (progn (message "coq is not V7") nil))))
+
 ;; Command to reset the Coq Proof Assistant
 ;; Pierre: added Impl... because of a bug of Coq until V6.3
 ;; (included). The bug is already fixed in the next version (V7). So