aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES23
1 files changed, 20 insertions, 3 deletions
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