Document Local Declare ML Module

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12674 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index be8b1404a5..a7dec737a7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -92,7 +92,8 @@ Vernacular commands
   done via new command "Declare Instance", while the syntax "Instance"
   now always provides a concrete instance, both in and out of Module Type.
 - Include Type is now deprecated since Include now accept both modules and
-  module types. 
+  module types.
+- Declare ML Module supports Local option.
 
 Tools