diff options
Diffstat (limited to 'dev/doc/changes.txt')
-rw-r--r-- | dev/doc/changes.txt | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index bb6c2f660..7fad65bf0 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -175,7 +175,7 @@ uses type classes and rejects terms with unresolved holes. functions that used to carry a suffix `_loc`, such suffix has been dropped. -- `errorlabstrm` has been removed in favor of `user_err`. +- `errorlabstrm` and `error` has been removed in favor of `user_err`. - The header parameter to `user_err` has been made optional. |