diff options
| author | Hugo Herbelin | 2015-04-01 21:32:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-04-01 22:46:16 +0200 |
| commit | 226bf474155092f41cbb0d3e47143ac221947342 (patch) | |
| tree | 38d1a422afef0bce84e1c50aa7db86d258e4f4f8 /doc/refman/RefMan-ext.tex | |
| parent | 81ce0dbd13a6d50b2a4e7617be3684db16b8b2f8 (diff) | |
Fixing a few typos + some uniformization of writing in doc.
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 85f191104e..cc5239a779 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1059,7 +1059,7 @@ names to {\Coq} names is needed. In this translation, names in the file system are called {\em physical} paths while {\Coq} names are contrastingly called {\em logical} names. -A logical prefix {\tt Lib} can associated to a physical path +A logical prefix {\tt Lib} can be associated to a physical path \textrm{\textsl{path}} using the command line option {\tt -Q} \textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are recursively associated to the logical path {\tt Lib} extended with the @@ -1102,8 +1102,8 @@ root to the required file (see~\ref{Require}). There also exists another independent loadpath mechanism attached to {\ocaml} object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files as described above. The {\ocaml} loadpath is managed using the option -\texttt{-I path}. As in the {\ocaml} world, there is neither a notion of logical -name prefix nor a way to access files in subdirectories of \texttt{path}. +\texttt{-I path} (in the {\ocaml} world, there is neither a notion of logical +name prefix nor a way to access files in subdirectories of \texttt{path}). See the command \texttt{Declare ML Module} in Section~\ref{compiled} to understand the need of the {\ocaml} loadpath. |