From 514403a0382b380be7acc5d3e0a5ec34d10fe227 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Fri, 25 Nov 2016 23:10:24 +0100 Subject: write CHANGES --- CHANGES | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/CHANGES b/CHANGES index 10cf0d25..dca879b3 100644 --- a/CHANGES +++ b/CHANGES @@ -12,6 +12,33 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac - Using query-replace (or replace-string) in the processed region doesn't wrongly jump to the first match anymore. +** Coq changes + +*** new menu Coq -> Auto Compilation for all background compilation options + +*** 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 + option `coq-compile-quick' or the subsection "11.3.3 Quick + compilation and .vio Files" in the Coq reference manual. + +*** bug fixes + - avoid leaving partial files behind when compilation fails + - 123: Parallel background compliation fails to execute some + imports + - fix error in process filter: Cannot resize window + - 54 partially: Buffer coq-compile-response sometimes takes + over the whole window + - 75: Library more.v is required + - 70: Coq trunk + compile before require => « Invalid version + syntax: 'trunk' » + - 92: Compile before require from current directory failing + with 8.5 + * Changes of Proof General 4.4 from Proof General 4.3 ** ProofGeneral has moved to GitHub! -- cgit v1.2.3