diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-03-11 12:09:03 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-03-11 12:09:03 +0000 |
| commit | 66004cbbdf3858f12482990af7b06291e676d262 (patch) | |
| tree | 4b4e7f8eb858cb64de8782f3598ebd4322e3fc16 /coq/coq-indent.el | |
| parent | 41c4820a778903785d2009820a06787d273152e4 (diff) | |
bug fixes on indenting and command-end-regexp.
Diffstat (limited to 'coq/coq-indent.el')
| -rw-r--r-- | coq/coq-indent.el | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index ab8f533d..7505b5ec 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -386,7 +386,9 @@ ; or from the command start (if we are in an Inductive type) ((proof-looking-at-safe coq-indent-pattern-regexp) (save-excursion (coq-find-unclosed 1 real-start) - (+ (current-column) proof-indent))) + (if (proof-looking-at-safe "\\s(") + (+ (current-indentation) proof-indent) + (+ (current-column) proof-indent)))) ; if we find a "then" we indent from the first unclosed if ; or from the command start (should not happen) |