Mis-a-jour modules, ajout de Import et Export

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

1 files changed, 6 insertions, 3 deletions

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index d420a269a..6a5dc3958 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -419,10 +419,13 @@ waste of time.
 % \SeeAlso sections \ref{Opaque}, \ref{loadpath}, chapter
 % \ref{Addoc-coqc}
 
-\subsection{\tt Import {\qualid}.}\comindex{Import}
-\label{Import}
+%\subsection{\tt Import {\qualid}.}\comindex{Import}
+%\label{Import}
 
-TODO + variant Export
+%%%%%%%%%%%%
+% Import and Export described in RefMan-mod.tex
+% the minor difference (to avoid multiple Exporting of libraries) in
+% the treatment of normal modules and libraries by Export omitted
 
 
 \subsection{\tt Require {\dirpath}.}