From 294c323165c26790c2dd57fdbea2de30278f1ca6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 May 2008 10:56:02 +0000 Subject: [PATCH] ... --- helm/software/matita/dist/ChangeLog | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index f6f973f03..baad226d1 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,10 +1,13 @@ 0.5.1 - -/5/2008 - minor bug fix release + * visualization of inductive types reports the number of fixed parameters * a wrong context was used to refine fixpoints arguments when trying to optimize out the letin (grep for `AvoidLetIn): (let rec f x = Fix... in f t ---> Fix... t) * auto fixed to prefer goals with metavariables to closed ones, added new syntax to specify the universe "auto by t1, t2, ...", updated documentation describing all auto parameters + * declarative language syntax and documentation ported to the new + auto parameters 0.5.0 - 9/5/2008 - bugfix release * first release not considered experimental -- 2.39.2