From 21debc12c6771bc00ed6ae1e1b37312e8205ec93 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 2 Mar 2020 14:48:21 +0100 Subject: [PATCH] Fix #462. Fixed making the lexer detect the number after "do". --- coq/coq-smie.el | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/coq/coq-smie.el b/coq/coq-smie.el index e960ff196..f07ad4ed0 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -523,6 +523,9 @@ The point should be at the beginning of the command name." ((member tok '("End")) (save-excursion (coq-smie-backward-token))) + ((member tok '("do")) + (save-excursion (coq-smie-backward-token-aux))) + ; empty token if a prenthesis is met. ((and (zerop (length tok)) (looking-at "{|")) (goto-char (match-end 0)) "{|") @@ -650,6 +653,15 @@ The point should be at the beginning of the command name." "|| tactic" "||")))))) + ;; This may be part of monadic notation, so detect other uses of "do". + ((equal tok "do") + (save-excursion + (forward-char 2) + (smie-default-forward-token) + (smie-default-backward-token) + (if (looking-at "[0-9]") "do ltac" + "do"))) + ; Same for "->" : rewrite or intro arg or term's implication ; FIXME: user defined arrows will be considered a term