diff options
| author | Pierre Courtieu | 2007-04-16 09:45:29 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2007-04-16 09:45:29 +0000 |
| commit | e9ad6746f96b5baa78df707ee29062dc2f3baa17 (patch) | |
| tree | 798bbdaf06ae413494ae3a6d4adf8aba95d6888e | |
| parent | 2384d0697a9993fdae02b53584488d486e15ade7 (diff) | |
Made coq version 8.1 the default.
| -rw-r--r-- | coq/coq-syntax.el | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index f20b7ad5..3265b501 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -29,11 +29,11 @@ ProofGeneral guesses the version of coq by doing 'coqtop -v'." ) (defvar coq-version-is-V8-1 nil "This variable can be set to t to force ProofGeneral to coq version -coq-8.1 (use it for coq-8.0cvs after january 2005). To do that, put -\(setq coq-version-is-V8-1 t) in your .emacs and restart emacs. This -variable cannot be true simultaneously with coq-version-is-V8-0. If -none of these 2 variables is set to t, then ProofGeneral guesses the -version of coq by doing 'coqtop -v'." ) +coq-8.1 and above(use it for coq-8.0cvs after january 2005). To do +that, put \(setq coq-version-is-V8-1 t) in your .emacs and restart +emacs. This variable cannot be true simultaneously with +coq-version-is-V8-0. If 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 @@ -66,6 +66,9 @@ version of coq by doing 'coqtop -v'." ) ((and num (string-match "\\<8.1" num)) (message v81) (setq coq-version-is-V8-1 t)) + ((and num (string-match "\\<8.2" num)) + (message (concat "coq version is 8.2: " v81)) + (setq coq-version-is-V8-1 t)) (t ; 8.1 by default now (message (concat "Falling back to default: " v81)) (setq coq-version-is-V8-1 t))))))))) |