Documenting the Shrink Abstract option.

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 08484a4b9b..547ec8f9e3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,8 @@ Tactics
 - New compatibility flag "Universal Lemma Under Conjunction" which
   let tactics working under conjunctions apply sublemmas of the form
   "forall A, ... -> A".
+- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
+  tactical w.r.t. variables appearing in the body of the proof.
 
 API