From: Enrico Tassi Date: Mon, 12 Oct 2009 16:00:29 +0000 (+0000) Subject: added last 10 months work... X-Git-Tag: make_still_working~3334 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c69505678c1746083a9a01ec4367cea67d888aa1;p=helm.git added last 10 months work... --- diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index 8a1ea5ce7..198920eac 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,3 +1,30 @@ +0.5.8 - ... - toward the 1.x series + * Complete rewriting of paramodulation code (thanks to Maxime Denes), + that is abstract over the data type embedded in the fisrt order + theory the procedure is able to handle. + Can be used as a stand-alone prover, and partecipated + to the CASC22 beating many older systems ;-) + * new (compact) kernel: + * toplevel fixpoints + * height (inter object dependency) driven conversion + * compact metavariable representation + * experimental irrelevant arguments handling in convesion + (in the spirit of proof irrelevance) + * explicit predicative universes + * new refiner: + * bi-directional type inference + * unification hints + * implicit vector (expands to the tight number of implicits) + * new basic tactics: + * new type for tactics, with a global view on the ongoing proof + * heavily based on the refiner + * work with terms labelled with their contexts + * new auto (prolog like) proof search tactic: + * works on a set of goals + * non uniform context support: + * arbitrary tactics can be called to attack a goal (hardcoded + at the OCaml level), for now just apply and intro + 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.