From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 17 Nov 2011 00:07:33 +0000 (+0000)
Subject: Towards 0.95.1.
X-Git-Tag: make_still_working~2097
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=01dc8db691f533de49f53dfdd173195336731c2b;p=helm.git

Towards 0.95.1.
---

diff --git a/matita/matita/dist/ChangeLog b/matita/matita/dist/ChangeLog
index dca7c2abf..90d654b7f 100644
--- a/matita/matita/dist/ChangeLog
+++ b/matita/matita/dist/ChangeLog
@@ -3,6 +3,10 @@
 	* new compact syntax for tactics
 	* improved automation
 	* experimental multi tabbed interface
+	* John Major equality and the computation version of the K axiom are
+	  now in the standard library
+	* generation of inversion/destruct principles using either
+	  Leibniz or John Major equalities
 	* several bug fixes
 
 0.5.7 - 15/02/2009 - Pàdoa release
diff --git a/matita/matita/dist/TODO b/matita/matita/dist/TODO
index 5305382b0..d75c433f3 100644
--- a/matita/matita/dist/TODO
+++ b/matita/matita/dist/TODO
@@ -2,13 +2,10 @@ TODO:
 - "ncoercion" statement:
   - simple syntax
   - generation of hints to implement the pullback
-- principles generation:
-  - induction/inversions
 - dependency graphs
 - queries (on the trie?)
 - Tactics:
-  - satuation
-  - destruct
+  - saturation
   - ncut
   - nclearbody
   - nletin che prende il tipo