aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES10
1 files changed, 9 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 3719481de..3fd784aff 100644
--- a/CHANGES
+++ b/CHANGES
@@ -47,7 +47,15 @@ Internal Infrastructure
many internal a.s.t. of Coq are now placed in mli files in
a new directory intf/, for instance constrexpr.mli or glob_term.mli.
More details in dev/doc/changes.
-
+- The file states/initial.coq does not exist anymore. Instead, coqtop
+ initially does a "Require" of Prelude.vo (or nothing when given
+ the options -noinit or -nois).
+- The build system does not produce anymore programs named coqtop.opt
+ and a symbolic link to coqtop. Instead, coqtop is now directly
+ an executable compiled with the best OCaml compiler available.
+ The bytecode program coqtop.byte is still produced. Same for other
+ utilities.
+
Changes from V8.4beta2 to V8.4
==============================