aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorHendrik Tews2020-04-12 11:30:58 +0200
committerPierre Courtieu2020-04-15 18:05:31 +0200
commit8273e22e6da7b20e51fa330116bee20964d5dab8 (patch)
tree5763a85a0a4ac5e4e2c93f477cb418b652f21ebc /CHANGES
parente38d79e7447ac8e561c9dbfe3ade8b8d1d2c06ad (diff)
add CHANGES entry for vos
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES19
1 files changed, 13 insertions, 6 deletions
diff --git a/CHANGES b/CHANGES
index 9713ea0e..39699d7f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,15 +29,22 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
*** new menu Coq -> Auto Compilation for all background compilation options
+*** support for 8.11 vos compilation
+
+ See menu Coq -> Auto Compilation -> vos compilation, option
+ coq-compile-vos and subsection "11.3.3 Quick and inconsistent
+ compilation" in the Coq reference manual.
+
*** support for 8.5 quick compilation
- See new menu Coq -> Auto Compilation. Select "no quick" as
- long as you have not switched to "Proof using" to compile
- without -quick. Select "quick no vio2vo" to use -quick
- without vio2vo (and guess what "quick and vio2vo" means ;-),
- select "ensure vo" to ensure a sound development. See the
+ See new menu Coq -> Auto Compilation -> Quick compilation.
+ Select "no quick" as long as you have not switched to "Proof
+ using" to compile without -quick. Select "quick no vio2vo" to
+ use -quick without vio2vo (and guess what "quick and vio2vo"
+ means ;-), select "ensure vo" to ensure a sound development.
+ Quick compilation is only supported for Coq < 8.11. See the
option `coq-compile-quick' or the subsection "11.3.3 Quick
- compilation and .vio Files" in the Coq reference manual.
+ and inconsistent compilation" in the Coq reference manual.
*** new option coq-compile-keep-going (in menu Coq -> Auto Compilation)