From 408cd15024070337ed4c0c5e093a4753c755cdb2 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 5 Feb 2003 22:35:39 +0000
Subject: New setting for parse cmdend regexp.

---
 coq/coq.el | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3