X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdist%2FChangeLog;h=8a1ea5ce78c6a0f32d1c68517c475bb0d3ad780f;hb=026c6c5b0e094b2e6e8244909bc5ac3d88b70b9c;hp=8f25732530bcee1fe617d4742ede034afe52cbde;hpb=689fa74fe440972f3b32ec7dbb6c3e49a68e26f0;p=helm.git diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index 8f2573253..8a1ea5ce7 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,3 +1,116 @@ +0.5.7 - 15/02/2009 - Pàdoa release + * are_convertible bug solved, arguments of application where + compared allowing cumulativity. This allowed to prove Type0=Type1. + * cases tactic speedup in the simplest case of an inductive type + hose right parameters have all to be abstracted when the outtype is + built + * maction support added to output notation (adopted for "=" that + expands to "= \sub T" to show the equality type) + * generation of derived lemmas rewritten to be based on hooks that + are triggered every definition + * composition of coercions fixed, more composite are generated + * undo mechanism for coercions remade, should work better + * new command "prefer coercion foo" to reorder coercions. + * UTF-8 eq classes and virtuals described in the manual and + consistently printed in the TeX/UTF-8 table + * added a memory system for UTF-8 equivalence classes, so that + last choice is remembered and attempted first next time the same + eq class is walked trough + * some core notation fixed to allow a better setoid-path + representation (foo ^-1 changed precedence) + * 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 + with VirtualBox + * 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 + symbols reducing the bounding box size + +0.5.6 - 1/12/2008 - bugfix release + * more abstract disambiguation algorithm, simpler instantiation + to a different CIC/refiner + * natural deduction support improved in the first order case + * natural deduction lem rule does now support lemmas + with (up to) 3 premises (multicut rule, displayed as + a collapsed tree) + +0.5.5 - 17/11/2008 - bugfix release with students in mind + * by ... we proved fixed to use only the specified lemmas but + using full unification inside auto. + * new apply rule tactic, that exploits the goal type to + disambiguate the input term. + * new didactic/ library directory, with support for natural deduction + treese. + +0.5.4 - 19/10/2008 - bugfix release + * When a file is opened, the cursor is placed at the begin of the + buffer and not atthe end as before + * New macro eval + * 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 + * coercion hiding now works properly for coercions to funclass + * triangular pullback works better with coercions to the function space + * notation for lists fixed to add a break point after the separator + * notation for the existential is now user definable + * \infrule layout added, allows to display readable fractions + * better window for terms grammar and TeX/Unicode + * fixed a bug in the positivity check not considering some subterms + * fixed some GUI glitches thanks to glade-3 + +0.5.2 - 2/7/2008 - better-usability-for-the-working-constructivist release + * refinement of match fixed to prevent useless unfolding, + head_beta_reduce is used instead of whd ~delta:true + * CProp hierarchy, interleaved with type (used to be a single universe) + * Notation now allows to set the precedence level of subterms, avoiding + unnecessary parenthese + * UTF-8 / TeX conversion table is now available in the Help menu + * Notation subsystem described in the manual + * EBNF term grammar is now available in the View menu (and is in sync with + the currently loaded notation) + * Rewrite tactic (in hypothesis) now computes the right sort and + uses the right equality elimination principle + * URI free interpretation and coercion statements (scripts are almost + relocatable now) + * elim and cases tactic now support a pattern to specify hypotheses that + are generalized before the elimination. + +0.5.1 - 29/5/2008 - minor bug fix release + * visualization of inductive types reports the number of fixed parameters + * a wrong context was used to refine fixpoints arguments + when trying to optimize out the letin (grep for `AvoidLetIn): + (let rec f x = Fix... in f t ---> Fix... t) + * auto fixed to prefer goals with metavariables to closed ones, + added new syntax to specify the universe "auto by t1, t2, ...", + updated documentation describing all auto parameters + * declarative language syntax and documentation ported to the new + auto parameters + 0.5.0 - 9/5/2008 - bugfix release * first release not considered experimental