diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2015-01-05 09:04:29 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2015-01-05 09:04:29 +0000 |
commit | 453c56a955f15623a29ae41a4e767b7745e80076 (patch) | |
tree | 6b633d479a3bcfe8e1263a4686c975aaac4476cc /CHANGES | |
parent | 22d7dccdd23603d07975799a159623223cb31095 (diff) |
trying to indent pending forall in the expected way
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 13 |
1 files changed, 13 insertions, 0 deletions
@@ -33,6 +33,19 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. Indentation supports only bullets of length <= 4 (like ----). Longer may be supported if needed. +*** by default, forall at the start of a lemma are not indented as a box + For instance, this is indented like this: + + Lemma foo: forall x y, + x = 0 -> ... . + + instead of: + + Lemma foo: forall x y, + x = 0 -> ... . + + Put (setq coq-indent-box-style t) to bring the box style back. + *** Support for bullets, braces and Grab Existential Variables for Prooftree. *** Support for _Coqproject files |