CHANGES update

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14082 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 63adca842..bf4673909 100644
--- a/CHANGES
+++ b/CHANGES
@@ -13,9 +13,9 @@ Logic
 Specification language and notations
 
 - Maximal implicit arguments can now be set locally by { }. The registration
-  traverses fixpoints and lambdas. Because there is conversion in types, 
+  traverses fixpoints and lambdas. Because there is conversion in types,
   maximal implicit arguments are not taken into account in partial
-  applications (use eta expansion instead).
+  applications (use eta expanded form with explicit { } instead).
 - Added support for recursive notations with binders (allows for instance
   to write "exists x y z, P").
 
@@ -109,6 +109,15 @@ Tools
   coqtop subprocess can be interrupted, or even killed and relaunched
   (cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts,
   the Windows version of coqide now requires Windows >= XP SP1.
+- coq_makefile major cleanup.
+  * mli are taken into account, ml aren't preproccessed anymore, ml4 really
+    work
+  * mlihtml generates doc of mli, install-doc install the html doc in DOCDIR
+    with the same policy as vo in COQLIB
+  * More variables are given by coqtop -config, others are defined only if the
+    users doesn't have defined them elsewhere. Consequently, generated makefile
+    should work directly on any architecture.
+  * Packager can take advantage of $(DSTROOT) introduction
 
 Changes from V8.2 to V8.3
 =========================