diff options
| author | Hendrik Tews | 2020-04-12 11:30:58 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-04-15 18:05:31 +0200 |
| commit | 8273e22e6da7b20e51fa330116bee20964d5dab8 (patch) | |
| tree | 5763a85a0a4ac5e4e2c93f477cb418b652f21ebc /CHANGES | |
| parent | e38d79e7447ac8e561c9dbfe3ade8b8d1d2c06ad (diff) | |
add CHANGES entry for vos
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 19 |
1 files changed, 13 insertions, 6 deletions
@@ -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) |
