Hint Cut documentation and cleanup of printing (was duplicated and

inconsistent).

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 019c6cdb24..af874bf1cc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,8 @@ Tactics
   of incompatibilities).
 - Hints costs are now correctly taken into account (potential source of
   incompatibilities).
+- Documented the Hint Cut command that allows control of the
+  proof-search during typeclass resolution (see reference manual).
 
 API