From d7cb0e2115ec37eddeeecbb1f2dbdeb7e49aeb7a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 15:16:46 +0100
Subject: Mention notypeclasses refine in CHANGES

---
 CHANGES | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 7f171ebc40..4a70584da7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,7 +75,10 @@ Tactics
 - Option "Injection On Proofs" was renamed "Keep Proof Equalities". When
   enabled, injection and inversion do not drop equalities between objects
   in Prop. Still disabled by default.
-
+- New tactics "notypeclasses refine" and "simple notypeclasses refine" that
+  disallow typeclass resolution when typechecking their argument, for use
+  in typeclass hints.
+  
 Hints
 
 - Revised the syntax of [Hint Cut] to follow standard notation for regexps.
-- 
cgit v1.2.3