From 82311da10ee3dfa6f29ddfb9225f9f05c29dca31 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 21 Apr 2021 00:23:00 +0200
Subject: Document the "Proof using" requirement for 'proof-omit-proofs-option

---
 CHANGES | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index e1f63e82..59566881 100644
--- a/CHANGES
+++ b/CHANGES
@@ -156,7 +156,11 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
     letting errors in these proofs go unnoticed. Configure
     `proof-omit-proofs-option' or select "Proof-General -> Quick
     Options -> Processing -> Omit Proofs". See also section
-    "11.5 Omitting proofs for speed" in the manual  
+    "11.5 Omitting proofs for speed" in the manual.
+
+    Beware that if lemmas are proved in a section, these lemmas should
+    start with a "Proof using" annotation, otherwise Coq would compute
+    a wrong type for them when this omitting-proofs feature is enabled.
 
 *** bug fixes
     - avoid leaving partial files behind when compilation fails
-- 
cgit v1.2.3