Update CHANGES

1 files changed, 10 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index fdd4feb598..9957ad17f7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,6 +40,15 @@ Tactics
 
 - Tactics and tactic notations now understand the `deprecated` attribute.
 
+Standard Library
+
+- Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
+  and proved some lemmas about them.  Note that this might cause
+  incompatibilities if you have, e.g., string_scope and Z_scope both
+  open with string_scope on top, and expect `=?` to refer to `Z.eqb`.
+  Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you
+  want).
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
@@ -99,7 +108,7 @@ SSReflect
   In particular rule 3 lets one write {x}/v even if v uses the variable x:
   indeed the view is executed before the renaming.
 
-- An empty clear switch is now accepted in intro patterns before a 
+- An empty clear switch is now accepted in intro patterns before a
   view application whenever the view is a variable.
   One can now write {}/v to mean {v}/v.  Remark that {}/x is very similar
   to the idiom {}e for the rewrite tactic (the equation e is used for