1 0.5.7 - .../12/2008 - PĂ doa release
2 * some core notation fixed to allow a better setoid-path
4 * matita manual updated with a section regarding the usage of
5 the liveCD with the VirtualBox emulator
6 * liveCD fixed to allow to easily mount/unmount real host folders
7 * ttf-freefont package added to the liveCD together with gucharmap
8 * coercions from convertible types are not inserted for real, they
9 just behave as hints for the unification algorithm
10 * virtuals (eq classes) fixed w.r.t. greek letters
11 * some virtuals added to ease the writing of diamond (<>), box ([])
13 * code that generates eliminators fixed to use whd ~delta set to true
14 when counting products, this allows to used definitions as inductive
16 * match ... with rendering fixed to break the box containing
17 constructors arguments if needed (i.e. record projections
18 are now almost readable)
19 * fixed pattern matching over ast terms, Ast.Case construct can be
20 matched correctly. Look the o-algebra example if you are
22 * Mpadded MathML tag can be used in notation, it allows to overlap
23 symbols reducing the bounding box size
25 0.5.6 - 1/12/2008 - bugfix release
26 * more abstract disambiguation algorithm, simpler instantiation
27 to a different CIC/refiner
28 * natural deduction support improved in the first order case
29 * natural deduction lem rule does now support lemmas
30 with (up to) 3 premises (multicut rule, displayed as
33 0.5.5 - 17/11/2008 - bugfix release with students in mind
34 * by ... we proved fixed to use only the specified lemmas but
35 using full unification inside auto.
36 * new apply rule tactic, that exploits the goal type to
37 disambiguate the input term.
38 * new didactic/ library directory, with support for natural deduction
41 0.5.4 - 19/10/2008 - bugfix release
42 * When a file is opened, the cursor is placed at the begin of the
43 buffer and not atthe end as before
45 * More code in the direction of a fully functional matita status, that
46 improved undo reliability in the parser/notation modules
47 * matitac was seldom compiling up-to-date files, fixed
48 * Memory consumption durin proof construction cut down using Lazy.t
50 * mstyle support in notation for text color, font size
51 * AutoGui now scales fonts to the correct user-requested size
52 * Non linear pattern matching from the level of terms to the
53 one of content in interpretation command (if the same variable name
54 is used, the two captured terms must be alpha equivalent to match)
56 0.5.3 - 23/7/2008 - bugfix release
57 * many fixes concerning the CProp hiearchy
58 * coercion database simplified
59 * coercion hiding now works properly for coercions to funclass
60 * triangular pullback works better with coercions to the function space
61 * notation for lists fixed to add a break point after the separator
62 * notation for the existential is now user definable
63 * \infrule layout added, allows to display readable fractions
64 * better window for terms grammar and TeX/Unicode
65 * fixed a bug in the positivity check not considering some subterms
66 * fixed some GUI glitches thanks to glade-3
68 0.5.2 - 2/7/2008 - better-usability-for-the-working-constructivist release
69 * refinement of match fixed to prevent useless unfolding,
70 head_beta_reduce is used instead of whd ~delta:true
71 * CProp hierarchy, interleaved with type (used to be a single universe)
72 * Notation now allows to set the precedence level of subterms, avoiding
73 unnecessary parenthese
74 * UTF-8 / TeX conversion table is now available in the Help menu
75 * Notation subsystem described in the manual
76 * EBNF term grammar is now available in the View menu (and is in sync with
77 the currently loaded notation)
78 * Rewrite tactic (in hypothesis) now computes the right sort and
79 uses the right equality elimination principle
80 * URI free interpretation and coercion statements (scripts are almost
82 * elim and cases tactic now support a pattern to specify hypotheses that
83 are generalized before the elimination.
85 0.5.1 - 29/5/2008 - minor bug fix release
86 * visualization of inductive types reports the number of fixed parameters
87 * a wrong context was used to refine fixpoints arguments
88 when trying to optimize out the letin (grep for `AvoidLetIn):
89 (let rec f x = Fix... in f t ---> Fix... t)
90 * auto fixed to prefer goals with metavariables to closed ones,
91 added new syntax to specify the universe "auto by t1, t2, ...",
92 updated documentation describing all auto parameters
93 * declarative language syntax and documentation ported to the new
96 0.5.0 - 9/5/2008 - bugfix release
97 * first release not considered experimental
99 0.4.98 - ??/11/2007 - bugfix release
100 * compiles against camlp5 >= 5.0
101 * changed lablgtksourceview module name since it is now part of lablgtk2
103 0.4.97 - 16/11/2007 - initial release