From 60db7ba0c5e5f7b773591f8b244d25f9ddbc5576 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 9 Jan 2015 10:32:22 +0000 Subject: Removing non-smie indentation + fix CHANGES. --- CHANGES | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 15900535..cdf312c0 100644 --- a/CHANGES +++ b/CHANGES @@ -33,18 +33,29 @@ 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: +*** smie indentation is now the only choice. + Old code removed. will work only if emacs >= 23.3. + +*** indentation now supports { at end of line: + example: + + assert (h:n = k). { + apply foo. + reflexivity. } + apply h. + +*** Default indentation of forall and exists is not boxed anymore + For instance, this is now indented like this: Lemma foo: forall x y, - x = 0 -> ... . + x = 0 -> ... . (* like if forall x y, was on its own line *) instead of: Lemma foo: forall x y, x = 0 -> ... . - Put (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. *** Support for bullets, braces and Grab Existential Variables for Prooftree. @@ -52,7 +63,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. According to Coq documentation, it is advised to use coq_makefile -f _CoqProject -o Makefile to build your Makefile automatically - from "profect file" _CoqProject. Such a file should contains the + from "profect file" _CoqProject. Such a file should contain the options to pass to coq_makefile, i.e. paths to add to coq load path (-I, -R) and other options to pass to coqc/coqtop (-arg). @@ -64,11 +75,6 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. the use of local file variables (which remains possible and overrides project file options). -*** Automatic insertion of "as" clauses. - - Should work for induction and destruct for now. Toggle this option - with Coq/Settings/Auto insert As. - *** Support for prettify-symbols-mode. * Changes of Proof General 4.2 from Proof General 4.1 -- cgit v1.2.3