aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2015-06-23 11:58:05 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2015-06-23 11:58:05 +0000
commit16c890ce19773c090193f6a4ed0f77342b471dde (patch)
tree667e64074d325e008efdc1ab76d178dba8d816dc /CHANGES
parent24ed134175091ef56997be780d280cd5daa84e2b (diff)
Update to CHANGE.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES8
1 files changed, 7 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 779f334a..589a1b08 100644
--- a/CHANGES
+++ b/CHANGES
@@ -72,10 +72,16 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
Lemma foo: forall x y,
x = 0 -> ... .
+
instead of:
+
Lemma foo: forall x y,
x = 0 -> ... .
- do this: (setq coq-indent-box-style t) to bring the box style back.
+ (do this: (setq coq-indent-box-style t) to bring the box style back).
+
+ Use (setq coq-smie-after-bolp-indentation 0) for a smaller indentation:
+ Lemma foo: forall x y,
+ x = 0 -> ... .
*** Default indentation cases of "match with" are now indented by 2 instead of 4.
"|" is indented by zero: