diff options
| author | Pierre Courtieu | 2013-07-10 14:58:48 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2013-07-10 14:58:48 +0000 |
| commit | ad5a025af110bd9bda1461c894ed1d0b90aa027d (patch) | |
| tree | 3f0dc4b89002899e61491b7614741d69ee60d063 | |
| parent | c3cf9716040b613afecab125a3de97f6a7052f05 (diff) | |
Fixing #476. Adding more keywords for indentation like Lemma.
| -rw-r--r-- | coq/coq-smie-lexer.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el index 43901ae5..a8e7a9ce 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -231,6 +231,7 @@ force indentation." (save-excursion ; FIXME add other commands that potentialy open goals (when (proof-looking-at "\\(Local\\|Global\\)?\ \\(Definition\\|Lemma\\|Theorem\\|Fact\\|Let\\|Class\ +\\|Proposition\\|Remark\\|Instance\\|Corollary\\|Goal\ \\|Add\\(\\s-+Parametric\\)?\\s-+Morphism\\)\\>") (coq-lonely-:=-in-this-command)))) @@ -468,7 +469,7 @@ The point should be at the beginning of the command name." (save-excursion (not (member (coq-smie-backward-token) ;; recursive call looking at the ptoken immediately before - '("." ". proofstart" "; tactic" "[" "]" "|" "=>" ;; => may be wrong here but rare (have "=> ltac"?) + '("." ". proofstart" "; tactic" "[" "]" "|" "=>" ;; => may be wrong here but rare (h0ave "=> ltac"?) "{ subproof" "} subproof" "- bullet" "+ bullet" "* bullet"))))) "quantif exists") |