From 242fa6a6b9e11d7c41537025e824ae546915c648 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 28 Aug 2001 16:59:46 +0000 Subject: 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"). --- coq/coq.el | 19 +++++++++++-------- 1 file 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 -- cgit v1.2.3