From b87b27011a061ead6eca7d8630ad3f59c45877e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Apr 2020 01:54:29 -0400
Subject: [dev] [doc] Changes.

---
 dev/doc/changes.md | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index eac8d86b0a..9498ab8bbb 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -9,6 +9,13 @@
 
 ### ML API
 
+Proof state and constant declaration:
+
+- A large consolidation of the API handling interactive and
+  non-interactive constant has been performed; low-level APIs are no
+  longer available, and the functionality of the `Proof_global` module
+  has been merged into `Declare`.
+
 Notations:
 
 - Most operators on numerals have moved to file numTok.ml.
@@ -68,7 +75,6 @@ Proof state:
   information related to the constant declaration. Some functions have
   been renamed from `start_proof` to `start_lemma`
 
-
   Plugins that require access to the information about currently
   opened lemmas can add one of the `![proof]` attributes to their
   `mlg` entry, which will refine the type accordingly. See
-- 
cgit v1.2.3