Document Local Declare ML Module

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

2 files changed, 8 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
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index fa5f472525..316a02f1bd 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -571,6 +571,12 @@ files is only possible under the bytecode version of {\tt coqtop}
 \ref{Addoc-coqc}), or when Coq has been compiled with a version of
 Objective Caml that supports native {\tt Dynlink} ($\ge$ 3.11).
 
+\begin{Variants}
+\item {\tt Local Declare ML Module {\str$_1$} .. {\str$_n$}.}\\
+  This variant is not exported to the modules that import the module
+  where they occur, even if outside a section.
+\end{Variants}
+
 \begin{ErrMsgs}
 \item \errindex{File not found on loadpath : \str}
 \item \errindex{Loading of ML object file forbidden in a native Coq}