1 files changed, 5 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 547ec8f9e..121d90694 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,6 +26,11 @@ Tactics
 - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
   tactical w.r.t. variables appearing in the body of the proof.
 
+Program
+
+- The "Shrink Obligations" flag now applies to all obligations, not only those
+solved by the automatic tactic.
+
 API
 
 - Some functions from pretyping/typing.ml and their derivatives were potential