From 2af210aeab374b6fcd55db2a155d897a17face0b Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Tue, 27 Jan 2015 09:27:09 +0000
Subject: Fixed a bug in script navigation. Updated CHANGE

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

(limited to 'coq/coq-indent.el')

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index da73f808..93feebca 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -391,7 +391,9 @@ and return nil."
 The point is put exactly after the end of previous command, or at the (point-min if
 there is no previous command)."
   (coq-script-parse-cmdend-backward)
-  (if (proof-looking-at "\\.\\s-\\|{\\|}") (forward-char 1)) ; else = no match found
+  (when
+      (proof-looking-at "\\.\\s-\\|{\\|}\\|\\++\\|\\*+\\|-+")
+    (forward-char (- (match-end 0) (match-beginning 0)))) ; else = no match found
   (point))
 
 
-- 
cgit v1.2.3