aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
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 339ac2d9b7..cc58222fbf 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -5,6 +5,10 @@
- Functions and types deprecated in 8.10 have been removed in Coq
8.11.
+- Type Decl_kinds.locality has been restructured, see commit
+ message. Main change to do generally is to change the flag "Global"
+ to "Global ImportDefaultBehavior".
+
## Changes between Coq 8.9 and Coq 8.10
### ML4 Pre Processing