Merge branch 'v8.5'

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 3a9b7b7b00..fa621f5e59 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,6 +40,9 @@ Program
 solved by the automatic tactic.
 - Importing Program no longer overrides the "exists" tactic (potential source
   of incompatibilities).
+- Hints costs are now correctly taken into account (potential source of
+  incompatibilities).
+
 
 API