diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2003-02-06 00:16:29 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2003-02-06 00:16:29 +0000 |
| commit | af8c12edab11c17df9e1913b8190c401f8e084d6 (patch) | |
| tree | e71d5e25b937e994f1679b2fa130f7d2a9364d99 /coq/coq.el | |
| parent | 7ba3e9f222495aa37c4fca8ab6146941d798ee51 (diff) | |
little change to proof-script-command-end-regexp, again, to deal with
coq-v6.2. In the next version we will remove support for coq < 7.0.
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 5 |
1 files changed, 1 insertions, 4 deletions
@@ -594,10 +594,7 @@ This is specific to coq-mode." (setq proof-terminal-char ?\.) (setq proof-script-command-end-regexp - ;;(if coq-version-is-V7 "[.]\\([ \t\n\r]\\)\\|[.]\\'" "[.]") - ;; da: could you check this, Pierre? If you like it - ;; please remove these comments. - "[.]\\([\\. \t\n\r\\']\\|\\'\\)") + (if coq-version-is-V7 "[.]\\([\\. \t\n\r\\']\\|\\'\\)" ".")) (setq proof-script-comment-start "(*") (setq proof-script-comment-end "*)") (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name |