From 8273e22e6da7b20e51fa330116bee20964d5dab8 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Sun, 12 Apr 2020 11:30:58 +0200
Subject: add CHANGES entry for vos

---
 CHANGES | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

(limited to 'CHANGES')

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)
 
-- 
cgit v1.2.3