From c4f85702f27d484b3cf8a09627c5cd5bd3ff2b6e Mon Sep 17 00:00:00 2001
From: coq
Date: Thu, 11 Dec 2003 19:42:29 +0000
Subject: 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
---
 doc/RefMan-oth.tex | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'doc/RefMan-oth.tex')

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index d420a269af..6a5dc3958e 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}.}
-- 
cgit v1.2.3