bug fixes on indenting and command-end-regexp.

2 files changed, 5 insertions, 3 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index ab8f533d..7505b5ec 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -386,7 +386,9 @@
   ; or from the command start (if we are in an Inductive type)
 	  ((proof-looking-at-safe coq-indent-pattern-regexp) 
 		(save-excursion (coq-find-unclosed 1 real-start)
-							 (+ (current-column) proof-indent)))
+							 (if (proof-looking-at-safe "\\s(")
+								  (+ (current-indentation) proof-indent)
+								  (+ (current-column) proof-indent))))
 
   ; if we find a "then" we indent from the first unclosed if
   ; or from the command start (should not happen)
diff --git a/coq/coq.el b/coq/coq.el
index 62e23bed..bea485be 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -725,9 +725,9 @@ This is specific to coq-mode."
 (defun coq-mode-config ()
 
   (setq proof-terminal-char ?\.)
-  (setq proof-script-command-end-regexp   ;"\\(\\w\\|\\s-\\|\\(\\.\\.\\)+\\)\\.[^\\w\\.]"
+  (setq proof-script-command-end-regexp
         (if coq-version-is-V7 
-            "\\(?:\\w\\|\\s-\\|\\(?:\\.\\.\\)+\\)\\.\\(\\s-\\|\\'\\)"
+            "\\(?:\\w\\|\\s-\\|\\s)\\|\\(?:\\.\\.\\)+\\)\\.\\(\\s-\\|\\'\\)"
           "[.]"))
   (setq proof-script-comment-start "(*")
   (setq proof-script-comment-end "*)")