...

diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog
index 17bd3330abe8f26017de6db53490e9352d3c9d99..f00f59e57847b0362da0bc66b6fe3be8d48eeb5f 100644 (file)
--- a/helm/software/matita/dist/ChangeLog
+++ b/helm/software/matita/dist/ChangeLog
@@ -24,6 +24,13 @@
          * non uniform context support:
            * arbitrary tactics can be called to attack a goal (hardcoded 
              at the OCaml level), for now just apply and intro
+       * new installation:
+         * the standard library (now we have two of them) is not
+           distributed pre-compiled
+         * standard library .ma files can be included from everywhere since
+           they are in a standard path
+         * including a file of the standard library triggers its compilation
+           in the user's space
 
 0.5.7 - 15/02/2009 - Pàdoa release
        * are_convertible bug solved, arguments of application where