Skip to content

Commit

Permalink
add CHANGES entry for vos
Browse files Browse the repository at this point in the history
  • Loading branch information
hendriktews authored and Matafou committed Apr 15, 2020
1 parent e38d79e commit 8273e22
Showing 1 changed file with 13 additions and 6 deletions.
19 changes: 13 additions & 6 deletions CHANGES
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down

0 comments on commit 8273e22

Please sign in to comment.