New setting for parse cmdend regexp.

1 files changed, 4 insertions, 1 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 9cd00a53..ad32135a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -594,7 +594,10 @@ This is specific to coq-mode."
 
   (setq proof-terminal-char ?\.)
   (setq proof-script-command-end-regexp   
-	(if coq-version-is-V7 "[.]\\([ \t\n\r]\\)\\|[.]\\'" "[.]"))
+        ;;(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]\\)")
   (setq proof-script-comment-start "(*")
   (setq proof-script-comment-end "*)")
   (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name