aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.md4
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index b1fdfafd3a..30a2967259 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -19,6 +19,10 @@ Names
Constant.make3 has been removed, use Constant.make2
Constant.repr3 has been removed, use Constant.repr2
+- `Names.transparent_state` has been moved to its own module `TransparentState`.
+ This module gathers utility functions that used to be defined in several
+ places.
+
Coqlib:
- Most functions from the `Coqlib` module have been deprecated in favor of