diff options
| author | Pierre Courtieu | 2013-05-29 15:59:04 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2013-05-29 15:59:04 +0000 |
| commit | 8be536fe303eb1061aee731a9830e577b4656ef9 (patch) | |
| tree | f8d853160bb596bb12c0742e36f94ef95b10cfc8 /coq | |
| parent | 89377cd6710cd377a05f5116356ca277338bae26 (diff) | |
Fixing a minor bug in indetation (exists is tactic and a quantifier).
Diffstat (limited to 'coq')
| -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 a3522b69..6a71cda8 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -463,7 +463,8 @@ The point should be at the beginning of the command name." (not (member (coq-smie-backward-token) ;; recursive call '("." ". proofstart" "; tactic" "[" "]" "|" - "{ subproof" "} subproof")))) + "{ subproof" "} subproof" "- bullet" "+ bullet" + "* bullet")))) "quantif exists")) ((equal tok "∀") "forall") ((equal tok "→") "->") |