aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/changes.md
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc/changes.md')
-rw-r--r--dev/doc/changes.md13
1 files changed, 13 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9d592ee879..d6d296f012 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,18 @@
## Changes between Coq 8.9 and Coq 8.10
+### ML API
+
+Names
+
+- Kernel names no longer contain a section path. They now have only two
+ components (module path and label), which led to some changes in the API:
+
+ KerName.make takes only 2 components
+ KerName.repr returns only 2 components
+ KerName.make2 is now KerName.make
+ Constant.make3 has been removed, use Constant.make2
+ Constant.repr3 has been removed, use Constant.repr2
+
## Changes between Coq 8.8 and Coq 8.9
### ML API