Documenting the need of the "DECLARE PLUGIN" statement.

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 6515d5d0f0..f5e83bdaed 100644
--- a/CHANGES
+++ b/CHANGES
@@ -194,6 +194,12 @@ Internal Infrastructure
     by option -vmbyteflags which expects a comma-separated argument.
   * The -coqtoolsbyteflags option is discontinued, see -no-custom instead.
 
+Miscellaneous
+
+- ML plugins now require a "DECLARE PLUGIN \"foo\"" statement. The "foo" name
+  must be exactly the name of the ML module that will be loaded through a
+  "Declare ML \"foo\"" command.
+
 Changes from V8.4beta2 to V8.4
 ==============================