aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2001-03-20 17:26:00 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2001-03-20 17:26:00 +0000
commitb058e5209bf4968b9f31edcd4149251e659bbd6b (patch)
tree6a28ebae345930c70bbc14ef2816a798716e2d29 /coq/coq.el
parent2c83131fb1cff2d435961cb5a68fc40b17887fa0 (diff)
Added the config var proof-script-command-end-regexp fot coq V7.
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el1
1 files changed, 1 insertions, 0 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 434f7792..070b55d3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -463,6 +463,7 @@ This is specific to coq-mode."
(defun coq-mode-config ()
(setq proof-terminal-char ?\.)
+ (setq proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)")
(setq proof-comment-start "(*")
(setq proof-comment-end "*)")
(setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name