summaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES10
1 files changed, 8 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index 01a81554..a789796c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -423,6 +423,7 @@ Tools
- New stand-alone .vo files verifier "coqchk".
- Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
- New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
+- The binary "parser" has been renamed to "coq-parser".
Miscellaneous
@@ -432,8 +433,13 @@ Miscellaneous
Whelp search tool.
- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
"Test Printing Let for ref" and "Test Printing If for ref".
-- An overhauled build system (new Makefiles); see dev/doc/build-system.txt
-- Add -browser option to configure script
+- An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
+- Add -browser option to configure script.
+- Build a shared library for the C part of Coq, and use it by default.
+ Bytecode executables are now pure. The behaviour is configurable with
+ the -coqrunbyteflags configure option.
+- Complexity tests can be skipped by setting the environment variable
+ COQTEST_SKIPCOMPLEXITY.
Changes from V8.1gamma to V8.1
==============================