fixed coq command-end expression-regexp to deal with the token '..'

1 files 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