aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/changes.md
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-04-02 13:22:11 +0200
committerEmilio Jesus Gallego Arias2019-05-10 01:57:54 +0200
commit1cdaa823aa2db2f68cf63561a85771bb98aec70f (patch)
tree4359c3c1051797f89202793e788ee145a0826521 /dev/doc/changes.md
parent8ee7a4a7003fc2c5b01e0d6041961b3da14c0c84 (diff)
[api] Remove 8.10 deprecations.
Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it.
Diffstat (limited to 'dev/doc/changes.md')
-rw-r--r--dev/doc/changes.md7
1 files changed, 7 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9e0d47651e..7221c3de56 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,10 @@
+## Changes between Coq 8.10 and Coq 8.11
+
+### ML API
+
+- Functions and types deprecated in 8.10 have been removed in Coq
+ 8.11.
+
## Changes between Coq 8.9 and Coq 8.10
### ML4 Pre Processing