helm/software/matita/dist/ChangeLog

   1 0.5.3  - ?/7/2008 - bugfix release
   2         * many fixes concerning the CProp hiearchy
   3         * coercion database simplified
   4         * coercion hiding now works properly for coercions to funclass
   5         * triangular pullback works better with coercions to the function space
   6
   7 0.5.2  - 2/7/2008 - better-usability-for-the-working-constructivist release
   8         * refinement of match fixed to prevent useless unfolding,
   9           head_beta_reduce is used instead of whd ~delta:true
  10         * CProp hierarchy, interleaved with type (used to be a single universe)
  11         * Notation now allows to set the precedence level of subterms, avoiding
  12           unnecessary parenthese
  13         * UTF-8 / TeX conversion table is now available in the Help menu
  14         * Notation subsystem described in the manual
  15         * EBNF term grammar is now available in the View menu (and is in sync with
  16           the currently loaded notation)
  17         * Rewrite tactic (in hypothesis) now computes the right sort and
  18           uses the right equality elimination principle
  19         * URI free interpretation and coercion statements (scripts are almost
  20           relocatable now)
  21         * elim and cases tactic now support a pattern to specify hypotheses that
  22           are generalized before the elimination.
  23
  24 0.5.1  - 29/5/2008 - minor bug fix release
  25         * visualization of inductive types reports the number of fixed parameters
  26         * a wrong context was used to refine fixpoints arguments
  27           when trying to optimize out the letin (grep for `AvoidLetIn):
  28           (let rec f x = Fix... in f t ---> Fix... t)
  29         * auto fixed to prefer goals with metavariables to closed ones,
  30           added new syntax to specify the universe "auto by t1, t2, ...",
  31                 updated documentation describing all auto parameters
  32         * declarative language syntax and documentation ported to the new
  33           auto parameters
  34
  35 0.5.0  - 9/5/2008 - bugfix release
  36         * first release not considered experimental
  37
  38 0.4.98 - ??/11/2007 - bugfix release
  39         * compiles against camlp5 >= 5.0
  40         * changed lablgtksourceview module name since it is now part of lablgtk2
  41
  42 0.4.97 - 16/11/2007 - initial release