1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 0b55183f3..30bea7a7b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,6 +22,10 @@ Tactics
   beta-iota-reduced after type-checking. This has an impact on the
   type of the variables that the tactic "refine" introduces in the
   context, producing types a priori closer to the expectations.
+- In "Tactic Notation" or "TACTIC EXTEND", entry "constr_with_bindings"
+  now uses type classes and rejects terms with unresolved holes, like
+  entry "constr" does. To get the former behavior use
+  "open_constr_with_bindings" (possible source of incompatibility.
 
 Vernacular Commands