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
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
21 * elim and cases tactic now support a pattern to specify hypotheses that
22 are generalized before the elimination.
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
35 0.5.0 - 9/5/2008 - bugfix release
36 * first release not considered experimental
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
42 0.4.97 - 16/11/2007 - initial release