From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
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 +++++++++
 dev/top_printers.ml | 2 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ab78b0956f..1a24f23e5a 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
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ba0c54407c..f9b4025866 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -181,7 +181,7 @@ let ppproofview p =
   pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)
-- 
cgit v1.2.3