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.

1 files changed, 10 insertions, 0 deletions

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