aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-06-22 21:06:01 +0200
committerPierre-Marie Pédrot2018-11-19 13:29:55 +0100
commitad5aea737ecc639c31dda84322b3550a4d380b47 (patch)
treec068b7493867b8fe0bab81e285bbc09adda1f7aa /dev
parent96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 (diff)
Proper record type and accessors for transparent states.
This is documented in dev/doc/changes.md.
Diffstat (limited to 'dev')
-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..9c5785758d 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 `TranspState`.
+ 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