diff options
Diffstat (limited to 'doc/RefMan-oth.tex')
| -rw-r--r-- | doc/RefMan-oth.tex | 9 |
1 files changed, 6 insertions, 3 deletions
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}.} |