summaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
commit113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (patch)
treec260a140410c796f113584a2f7e6b9b7f6e00aa5 /CHANGES
parent870075f34dd9fa5792bfbf413afd3b96f17e76a0 (diff)
Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg
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
==============================