Documentation of the "Local Definition" command.

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

1 files changed, 16 insertions, 0 deletions

diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 68d572265..f4a90740c 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -372,6 +372,22 @@ Some features defined in modules are activated only when a module is
 imported. This is for instance the case of notations (see
 Section~\ref{Notation}).
 
+Declarations made with the {\tt Local} flag are never imported by the
+{\tt Import} command. Such declarations are only accessible through their
+fully qualified name.
+
+Example:
+
+\begin{coq_example}
+Module A.
+Module B.
+Local Definition T := nat.
+End B.
+End A.
+Import A.
+Check B.T.
+\end{coq_example}
+
 \begin{Variants}
 \item{\tt Export {\qualid}}\comindex{Export}