aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-smie.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-04 14:34:09 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-04 14:34:09 +0000
commit69198d98ee274af7ab60e26d93a4078c540c9e59 (patch)
treefd5d663c01f8e739870f0f8c81f6a707d5549389 /coq/coq-smie.el
parent4e0cdecdc3fa43dc07585ac05334bb6c9a3e622a (diff)
Fixed Proof end/start detection on Proof using ...
Was making scripting confused. P.
Diffstat (limited to 'coq/coq-smie.el')
-rw-r--r--coq/coq-smie.el2
1 files changed, 1 insertions, 1 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