From 85d5b246b0fbf845c6c61ffac6f0e2563c237d69 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 26 Jul 2018 09:54:42 -0400
Subject: Update CHANGES

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

diff --git a/CHANGES b/CHANGES
index a42c44c09b..b1f9d46ed8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -65,6 +65,15 @@ Standard Library
 
 - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it.
 
+- The scopes `int_scope` and `uint_scope` have been renamed to
+  `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect
+  and other packages.  They are still delimited by `%int` and `%uint`.
+
+- Numeral syntax for `nat` is no longer available without loading the
+  entire prelude (`Require Import Coq.Init.Prelude`).  This only
+  impacts users running Coq without the init library (`-nois` or
+  `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
@@ -98,6 +107,8 @@ Vernacular Commands
   overwritting the opacity set of the hint database.
 - Added generic syntax for “attributes”, as in:
   `#[local] Lemma foo : bar.`
+- Added the `Numeral Notation` command for registering decimal numeral
+  notations for custom types
 - The `Set SsrHave NoTCResolution` command no longer has special global
   scope. If you want the previous behavior, use `Global Set SsrHave
   NoTCResolution`.
-- 
cgit v1.2.3