diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 6 |
2 files changed, 8 insertions, 1 deletions
@@ -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} |