From c991cd766e22195cac3a3d9f0150af7a9301cc99 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Dec 2008 21:32:18 +0000 Subject: [PATCH] ... --- helm/software/matita/dist/ChangeLog | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index 9013f0550..4a1168c97 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,14 +1,25 @@ -0.5.7 - ... - ... - * code that generates eliminators fixed to use whd ~delta:true - when counting products, this allows to used definitions as inductive type - ariety. +0.5.7 - .../12/2008 - Pàdoa release + * some core notation fixed to allow a better setoid-path + representation + * matita manual updated with a section regarding the usage of + the liveCD with the VirtualBox emulator + * liveCD fixed to allow to easily mount/unmount real host folders + * ttf-freefont package added to the liveCD together with gucharmap + * coercions from convertible types are not inserted for real, they + just behave as hints for the unification algorithm + * virtuals (eq classes) fixed w.r.t. greek letters + * some virtuals added to ease the writing of diamond (<>), box ([]) + and upper bar (_). + * code that generates eliminators fixed to use whd ~delta set to true + when counting products, this allows to used definitions as inductive + type ariety. * match ... with rendering fixed to break the box containing constructors arguments if needed (i.e. record projections are now almost readable) * fixed pattern matching over ast terms, Ast.Case construct can be matched correctly. Look the o-algebra example if you are intereseted. - * mpadded mathml tag can be used in notation, it allows to overlap + * Mpadded MathML tag can be used in notation, it allows to overlap symbols reducing the bounding box size 0.5.6 - 1/12/2008 - bugfix release -- 2.39.2