Fixed Proof end/start detection on Proof using ...

Was making scripting confused.
P.

2 files changed, 5 insertions, 6 deletions

diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 993674b6..9a7df711 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -106,7 +106,7 @@ the token of \".\" is simply \".\"."
        ((looking-at "Proof\\>")
 	(forward-char 5)
 	(coq-find-not-in-comment-forward "[^[:space:]]") ;; skip spaces and comments
-	(if (looking-at "\\.\\|with") ". proofstart" "."))
+	(if (looking-at "\\.\\|with\\|using") ". proofstart" "."))
        ((or (looking-at "Next\\s-+Obligation\\>")
 	    (coq-smie-detect-goal-command))
 	(save-excursion
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index a4e11ba1..9075c1e1 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -741,7 +741,7 @@ Used by `coq-goal-command-p'"
 (defun coq-section-command-p (str)
   (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str))
 
-
+;; unused anymore (for good)
 (defun coq-goal-command-str-p (str)
   "Decide syntactically whether STR is a goal start or not. Use
 `coq-goal-command-p' on a span instead if possible."
@@ -776,7 +776,8 @@ Used by `coq-goal-command-p'"
         (or (coq-section-command-p str)
             (coq-module-opening-p str)))))
 
-;; TODO: rely on coq response nistead for span grouping
+;; TODO: rely on coq response nistead for span grouping Or better have
+;; coq change its syntax for something better.
 (defvar coq-keywords-save-strict
   '("Defined" "Save" "Qed" "End" "Admitted" "Abort" )
   "This regexp must match *exactly* commands that close a goal/Module.
@@ -793,9 +794,7 @@ It is used:
   "Decide whether argument is a Save command or not"
   (or (proof-string-match coq-save-command-regexp-strict str)
       (and (proof-string-match "\\`Proof\\>" str)
-           (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str)))
-      )
-  )
+           (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\|using\\)" str)))))
 
 
 ;; ----- keywords for font-lock.