1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 673649ee91..8d0623f585 100644
--- a/CHANGES
+++ b/CHANGES
@@ -52,6 +52,8 @@ Vernacular commands
 - The undocumented and obsolete option "Set/Unset Boxed Definitions" has
   been removed, as well as syntaxes like "Boxed Fixpoint foo".
 - A new option "Set Default Timeout n / Unset Default Timeout".
+- Qed now uses information from the reduction tactics used in proof script
+  to avoid conversion at Qed time to go into a very long computation.
 
 Module System