Final implementation of proof irrelevant conversion, which hadn't

[helm.git] / helm / software / matita / dist / ChangeLog

diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog
index 2ff51705c3121e12ff09f347ab625e30bb46c2b6..66d728fa3b638bf0b4987659b365251d8dc43e75 100644 (file)
--- a/helm/software/matita/dist/ChangeLog
+++ b/helm/software/matita/dist/ChangeLog
@@ -1,3 +1,15 @@
+0.5.v  - dd/mm/yyy - bugfix release
+       * More code in the direction of a fully functional matita status, that
+         improved undo reliability in the parser/notation modules
+       * matitac was seldom compiling up-to-date files, fixed
+       * Memory consumption durin proof construction cut down using Lazy.t
+         proof terms
+       * mstyle support in notation for text color, font size
+       * AutoGui now scales fonts to the correct user-requested size 
+       * Non linear pattern matching from the level of terms to the
+         one of content in interpretation command (if the same variable name
+         is used, the two captured terms must be alpha equivalent to match)
+
 0.5.3  - 23/7/2008 - bugfix release
        * many fixes concerning the CProp hiearchy
        * coercion database simplified