From 490704f4b2db98f4ef15f5e380b63e49e13a418b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Nov 2019 16:04:45 +0100
Subject: Moving the diversity of constr printers to a label style.

This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
---
 dev/doc/changes.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 7d394c3401..04b20c6889 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,15 @@
 ## Changes between Coq 8.11 and Coq 8.12
 
+### ML API
+
+Printers:
+
+- Functions such as Printer.pr_lconstr_goal_style_env have been
+  removed, use instead functions such as pr_lconstr with label
+  `goal_concl_style:true`. Functions such as
+  Constrextern.extern_constr which were taking a boolean argument for
+  the goal style now take instead a label.
+
 ## Changes between Coq 8.10 and Coq 8.11
 
 ### ML API
-- 
cgit v1.2.3