From 7f7e567188ea40fb396c1802224b7290b9e873a3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 13 Jul 2018 19:11:13 -0400
Subject: Update CHANGES

---
 CHANGES | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3