From d672652f4acb78b83403b080665e6c56e00f4feb Mon Sep 17 00:00:00 2001
From: Paul Steckler <steck@stecksoft.com>
Date: Fri, 26 Jan 2018 14:39:26 -0500
Subject: look for vernac controls before focus bracket, fix for #223

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

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 95b982ef..b6b8c18d 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -378,7 +378,14 @@ Comments are ignored, of course."
       (coq-empty-command-p))
      ;; other bulleting syntax
      ((looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p))
-     ;; not a bullet, we foound something else, it shoulf be either a
+     ;; vernacular controls Time, Fail, Redirect, Timeout
+     ((or (and (looking-at "e\\>") (looking-back "\\<Tim") (- (point) 3))
+          (and (looking-at "l\\>") (looking-back "\\<Fai") (- (point) 3))
+          (and (looking-at "\"") (looking-back "\\<Redirect\\s-+\"[^\"]+"))
+          (and (looking-at "[[:digit:]]\\_>") (looking-back "\\<Timeout\\s-+[[:digit:]]*")))
+      (goto-char (match-beginning 0))
+      (coq-empty-command-p))
+     ;; not a bullet, we found something else, it should be either a
      ;; dot or the beginning of the file, otherwise we are in the
      ;; middle of a command
      (t (looking-at "\\.\\|\\`"))
-- 
cgit v1.2.3