]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 12 Oct 2009 20:08:36 +0000 (20:08 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 12 Oct 2009 20:08:36 +0000 (20:08 +0000)
helm/software/matita/dist/ChangeLog

index 17bd3330abe8f26017de6db53490e9352d3c9d99..f00f59e57847b0362da0bc66b6fe3be8d48eeb5f 100644 (file)
          * 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