From 7628af7af9ff20d2a894673f66c3753e214623f1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 29 Dec 2017 20:20:38 +0100
Subject: [print] Restrict use of "debug" Termops printer.

The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.

We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.
---
 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 4f3d793ed4..fdeb0abed4 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,12 @@
+## Changes between Coq 8.9 and Coq 8.10
+
+### ML API
+
+Termops:
+
+- Internal printing functions have been placed under the
+  `Termops.Internal` namespace.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
-- 
cgit v1.2.3