From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 01:58:04 +0200
Subject: Remove errorlabstrm in favor of user_err

As noted by @ppedrot, the first is redundant. The patch is basically a renaming.

We didn't make the component optional yet, but this could happen in a
future patch.
---
 dev/doc/changes.txt | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index ac874befd1..699130944a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,11 +2,15 @@
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
 
+* ML API *
+
 ** Error handling **
 
-All error functions now take an optional parameter `?loc:Loc.t`. For
-functions that used to carry a suffix `_loc`, such suffix has been
-dropped.
+- All error functions now take an optional parameter `?loc:Loc.t`. For
+  functions that used to carry a suffix `_loc`, such suffix has been
+  dropped.
+
+- `errorlabstrm` has been removed in favor of `user_err`.
 
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
-- 
cgit v1.2.3