From 1dc24b8e6a2f307046dd64c1cd4d3b68c90de971 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 6 Jul 2012 20:47:09 +0000 Subject: More fixes in coq indentation. --- CHANGES | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 1cdc0f03..6783e253 100644 --- a/CHANGES +++ b/CHANGES @@ -24,9 +24,26 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** Support proof-tree visualization *** Indentation improvements using SMIE - Limitations: -**** hard-wired precedence between bullets - < + < * -**** no "{" following a bullet. + Still experimental. + +** Limitations: + +**** hard-wired precedence between bullets: - < + < * + example: + Proof. + - split. + + split. + * auto. + * auto. + + intros. + auto. + - auto. + Qed. + +**** Always use "Proof." when proving an "Instance". + (wrong indentation and slow downs otherwise) + As a general rule, try to always introduce a proof with "Proof." + (or "Next Obligation"). *** Minor parsing fixes -- cgit v1.2.3