aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Stefan Monnier <monnier@iro.umontreal.ca>2014-06-04 12:22:43 +0000
committerGravatar Stefan Monnier <monnier@iro.umontreal.ca>2014-06-04 12:22:43 +0000
commit1c0b0d32f95d7555943ab86a2de6666e39e84c13 (patch)
tree873351c01f6d74be8753d5f24b834664e2231fab /generic
parent67f4332c9e802a0d272ac0670515d98d16cfebb4 (diff)
* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.
(coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=".
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-shell.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index cc7e56f8..a8e79fcd 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -863,7 +863,7 @@ used in `proof-add-to-queue' when we start processing a queue, and in
;; Replace CRs from string with spaces to avoid spurious prompts.
(if proof-shell-strip-crs-from-input
- (setq string (subst-char-in-string ?\n ?\ string t)))
+ (setq string (subst-char-in-string ?\n ?\ string)))
(insert string)