diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/doc/changes.md | 6 |
2 files changed, 6 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 6f54ecb241..67a7e87d78 100644 --- a/dev/base_include +++ b/dev/base_include @@ -99,7 +99,6 @@ open Evarutil open Evarsolve open Tacred open Evd -open Universes open Termops open Namegen open Indrec diff --git a/dev/doc/changes.md b/dev/doc/changes.md index d6d296f012..7e64f80ac5 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,12 @@ ### ML API +General deprecation + +- All functions marked [@@ocaml.deprecated] in 8.8 have been + removed. Please, make sure your plugin is warning-free in 8.8 before + trying to port it over 8.9. + Names - Kernel names no longer contain a section path. They now have only two |