From 41c4820a778903785d2009820a06787d273152e4 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 10 Mar 2004 18:54:34 +0000
Subject: fixed coq command-end expression-regexp to deal with the token '..'

---
 coq/coq.el | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index c79f719c..62e23bed 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -725,8 +725,10 @@ This is specific to coq-mode."
 (defun coq-mode-config ()
 
   (setq proof-terminal-char ?\.)
-  (setq proof-script-command-end-regexp   
-        (if coq-version-is-V7 "[.]+\\([\\. \t\n\r]\\|\\'\\)" "[.]"))
+  (setq proof-script-command-end-regexp   ;"\\(\\w\\|\\s-\\|\\(\\.\\.\\)+\\)\\.[^\\w\\.]"
+        (if coq-version-is-V7 
+            "\\(?:\\w\\|\\s-\\|\\(?:\\.\\.\\)+\\)\\.\\(\\s-\\|\\'\\)"
+          "[.]"))
   (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