added last 10 months work...

diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog
index 8a1ea5ce78c6a0f32d1c68517c475bb0d3ad780f..198920eac7e5216a0b67fde861a5b53b9e00095b 100644 (file)
--- 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.