aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el25
1 files changed, 2 insertions, 23 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 1240eda5..2c0c3562 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -24,29 +24,8 @@
(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 (useful for
-;; people dealing with several version of coq) We also have coq-version-is-V74, to
-;; deal with the new module system
-(cond
- ((boundp 'coq-version-is-V74) (setq coq-version-is-V7 t))
- ((boundp 'coq-version-is-V7) (setq coq-version-is-V74 nil))
- (t
- (let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
- (x (string-match "version \\([.0-9]*\\)" str))
- (num (match-string 1 str)))
- (cond
- ((string-match num "\\<6.")
- (message "coq is V6") (setq coq-version-is-V7 nil) (setq coq-version-is-V74 nil))
- ((or (string-match num "\\<7.0") (string-match num "\\<7.1")
- (string-match num "\\<7.2") (string-match num "\\<7.3"))
- (message "coq is V7 =< 7.3")
- (setq coq-version-is-V7 t) (setq coq-version-is-V74 nil))
- ;default: 7.3.1 and above ---> 7.4
- (t (message "coq is => V7.3.1")
- (setq coq-version-is-V7 t) (setq coq-version-is-V74 t))))))
-
+;; da 15/02/03: moved setting of coq-version-is-vX to coq-syntax to
+;; fix compilation
(require 'coq-syntax)
;; Command to reset the Coq Proof Assistant