From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 31 Mar 2018 17:43:18 +0200
Subject: Evar maps contain econstrs.

We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
---
 dev/doc/changes.md | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ab78b0956..1a24f23e5 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,12 @@
+## Changes between Coq 8.8 and Coq 8.9
+
+### ML API
+
+Proof engine
+
+  More functions have been changed to use `EConstr`, notably the
+  functions in `Evd`.
+
 ## Changes between Coq 8.7 and Coq 8.8
 
 ### Bug tracker
-- 
cgit v1.2.3