diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2000-11-23 10:25:16 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2000-11-23 10:25:16 +0000 |
| commit | c0e191dfe45e32dd49ab704b52a76d17fa40d52a (patch) | |
| tree | ffba1706555b32d439e49b0211a52b7ac84b2a9f /coq | |
| parent | 7bc4491268808bb6dd8c45a66b46683eeac1940c (diff) | |
I am starting to make PG coqV7 compatible, I think the best is to
allow both V6 and V7 for a while. Theoretically, incompatibilities
will not be numerous.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 5 |
2 files changed, 6 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 5e559ea9..898cc17d 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -257,7 +257,7 @@ "Punctuation Symbols used by Coq") ;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\|Anomaly\\|Uncaught exception\\)" +(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\|Anomaly\\|Uncaught exception\\|Toplevel input\\)" "A regular expression indicating that the Coq process has identified an error.") @@ -18,6 +18,11 @@ "/usr/local/lib/coq" c))) +;;Pierre: we will have both versions V6 and V7 during a while +(setq coq-version-is-V7 + (let ((c (substring (shell-command-to-string "coqtop -v") 0 -1 ))) + (if (string-match "version 7" c) t nil))) + (defcustom coq-tags (concat (coq-library-directory) "/theories/TAGS") "the default TAGS table for the Coq library" :type 'string |