diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-03-15 10:26:12 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-03-15 10:26:12 +0000 |
| commit | af0373306857ae7ec403a0872974a4ea4a4da4a1 (patch) | |
| tree | 0d649e537ddce9c9cab05d4ac9c618da252ecbac /coq/coq-indent.el | |
| parent | f86882c6352c97753f74883cfeb4f17dab8d2f34 (diff) | |
little bug fix in coq-indent.el
Diffstat (limited to 'coq/coq-indent.el')
| -rw-r--r-- | coq/coq-indent.el | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 7505b5ec..3597c329 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -1,4 +1,4 @@ -;; coq-syntax.el indentation stuff for Coq +; coq-syntax.el indentation stuff for Coq ;; Copyright (C) 1997, 1998 LFCS Edinburgh. ;; Authors: Pierre Courtieu ;; Maintainer: Pierre Courtieu <courtieu@lri.fr> @@ -323,7 +323,7 @@ ; we are at an end command -> one ident left ; FIX: we should count the number of closing item on the line - ((coq-save-command-p (coq-current-command-string)) + ((coq-save-command-p nil (coq-current-command-string)) (- proof-indent)) ((proof-looking-at-safe "\\<Proof\\>") 0) ; no indentation at "Proof ..." @@ -334,7 +334,7 @@ (or (and ;"Proof ..." is a proof start (but not really a goal command) ; unless followed by a term (catch by coq-save-command-p above (proof-looking-at-safe "\\<Proof\\>") - (not (coq-save-command-p (coq-current-command-string)))) + (not (coq-save-command-p nil (coq-current-command-string)))) (coq-goal-command-p (coq-current-command-string)))) proof-indent) |