aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-08-19 02:35:47 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-08-19 02:46:38 +0200
commitfc579fdc83b751a44a18d2373e86ab38806e7306 (patch)
treeb325c2ff65c505ad62ac7b3fce6bce28633a60f0 /dev
parent543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff)
Make the user_err header an optional parameter.
Suggested by @ppedrot
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.txt2
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 699130944..7d5e3d1fe 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -12,6 +12,8 @@
- `errorlabstrm` has been removed in favor of `user_err`.
+- The header parameter to `user_err` has been made optional.
+
=========================================
= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
=========================================