matita/matita/dist/ChangeLog

   1 0.95.1 - 17/11/2011 - alpha version for the 1.x series
   2         * old kernel, unification, etc. removed
   3         * new compact syntax for tactics
   4         * improved automation
   5         * experimental multi tabbed interface
   6         * John Major equality and the computation version of the K axiom are
   7           now in the standard library
   8         * generation of inversion/destruct principles using either
   9           Leibniz or John Major equalities
  10         * several bug fixes
  11
  12 0.5.7 - 15/02/2009 - Pàdoa release
  13         * are_convertible bug solved, arguments of application where
  14           compared allowing cumulativity. This allowed to prove Type0=Type1.
  15         * cases tactic speedup in the simplest case of an inductive type
  16           hose right parameters have all to be abstracted when the outtype is
  17           built
  18         * maction support added to output notation (adopted for "=" that
  19           expands to "= \sub T" to show the equality type)
  20         * generation of derived lemmas rewritten to be based on hooks that
  21           are triggered every definition
  22         * composition of coercions fixed, more composite are generated
  23         * undo mechanism for coercions remade, should work better
  24         * new command "prefer coercion foo" to reorder coercions.
  25         * UTF-8 eq classes and virtuals described in the manual and
  26           consistently printed in the TeX/UTF-8 table
  27         * added a memory system for UTF-8 equivalence classes, so that
  28           last choice is remembered and attempted first next time the same
  29           eq class is walked trough
  30         * some core notation fixed to allow a better setoid-path
  31           representation (foo ^-1 changed precedence)
  32         * matita manual updated with a section regarding the usage of
  33           the liveCD with the VirtualBox emulator
  34         * liveCD fixed to allow to easily mount/unmount real host folders
  35           with VirtualBox
  36         * ttf-freefont package added to the liveCD together with gucharmap
  37         * coercions from convertible types are not inserted for real, they
  38           just behave as hints for the unification algorithm
  39         * virtuals (eq classes) fixed w.r.t. greek letters
  40         * some virtuals added to ease the writing of diamond (<>), box ([])
  41           and upper bar (_).
  42         * code that generates eliminators fixed to use whd ~delta set to true
  43           when counting products, this allows to used definitions as inductive
  44           type ariety.
  45         * match ... with rendering fixed to break the box containing
  46           constructors arguments if needed (i.e. record projections
  47           are now almost readable)
  48         * fixed pattern matching over ast terms, Ast.Case construct can be
  49           matched correctly. Look the o-algebra example if you are
  50           intereseted.
  51         * Mpadded MathML tag can be used in notation, it allows to overlap
  52           symbols reducing the bounding box size
  53
  54 0.5.6 - 1/12/2008 - bugfix release
  55         * more abstract disambiguation algorithm, simpler instantiation
  56           to a different CIC/refiner
  57         * natural deduction support improved in the first order case
  58         * natural deduction lem rule does now support lemmas
  59           with (up to) 3 premises (multicut rule, displayed as
  60           a collapsed tree)
  61
  62 0.5.5  - 17/11/2008 - bugfix release with students in mind
  63         * by ... we proved fixed to use only the specified lemmas but
  64           using full unification inside auto.
  65         * new apply rule tactic, that exploits the goal type to
  66           disambiguate the input term.
  67         * new didactic/ library directory, with support for natural deduction
  68           treese.
  69
  70 0.5.4  - 19/10/2008 - bugfix release
  71         * When a file is opened, the cursor is placed at the begin of the
  72           buffer and not atthe end as before
  73         * New macro eval
  74         * More code in the direction of a fully functional matita status, that
  75           improved undo reliability in the parser/notation modules
  76         * matitac was seldom compiling up-to-date files, fixed
  77         * Memory consumption durin proof construction cut down using Lazy.t
  78           proof terms
  79         * mstyle support in notation for text color, font size
  80         * AutoGui now scales fonts to the correct user-requested size
  81         * Non linear pattern matching from the level of terms to the
  82           one of content in interpretation command (if the same variable name
  83           is used, the two captured terms must be alpha equivalent to match)
  84
  85 0.5.3  - 23/7/2008 - bugfix release
  86         * many fixes concerning the CProp hiearchy
  87         * coercion database simplified
  88         * coercion hiding now works properly for coercions to funclass
  89         * triangular pullback works better with coercions to the function space
  90         * notation for lists fixed to add a break point after the separator
  91         * notation for the existential is now user definable
  92         * \infrule layout added, allows to display readable fractions
  93         * better window for terms grammar and TeX/Unicode
  94         * fixed a bug in the positivity check not considering some subterms
  95         * fixed some GUI glitches thanks to glade-3
  96
  97 0.5.2  - 2/7/2008 - better-usability-for-the-working-constructivist release
  98         * refinement of match fixed to prevent useless unfolding,
  99           head_beta_reduce is used instead of whd ~delta:true
 100         * CProp hierarchy, interleaved with type (used to be a single universe)
 101         * Notation now allows to set the precedence level of subterms, avoiding
 102           unnecessary parenthese
 103         * UTF-8 / TeX conversion table is now available in the Help menu
 104         * Notation subsystem described in the manual
 105         * EBNF term grammar is now available in the View menu (and is in sync with
 106           the currently loaded notation)
 107         * Rewrite tactic (in hypothesis) now computes the right sort and
 108           uses the right equality elimination principle
 109         * URI free interpretation and coercion statements (scripts are almost
 110           relocatable now)
 111         * elim and cases tactic now support a pattern to specify hypotheses that
 112           are generalized before the elimination.
 113
 114 0.5.1  - 29/5/2008 - minor bug fix release
 115         * visualization of inductive types reports the number of fixed parameters
 116         * a wrong context was used to refine fixpoints arguments
 117           when trying to optimize out the letin (grep for `AvoidLetIn):
 118           (let rec f x = Fix... in f t ---> Fix... t)
 119         * auto fixed to prefer goals with metavariables to closed ones,
 120           added new syntax to specify the universe "auto by t1, t2, ...",
 121                 updated documentation describing all auto parameters
 122         * declarative language syntax and documentation ported to the new
 123           auto parameters
 124
 125 0.5.0  - 9/5/2008 - bugfix release
 126         * first release not considered experimental
 127
 128 0.4.98 - ??/11/2007 - bugfix release
 129         * compiles against camlp5 >= 5.0
 130         * changed lablgtksourceview module name since it is now part of lablgtk2
 131
 132 0.4.97 - 16/11/2007 - initial release