diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/coqdoc.tex | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index 626593fc9d..e00484e6c1 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -386,10 +386,16 @@ Default behavior is to build an index, for the HTML output only, into Do not insert links to the \Coq\ standard library. +\item[\texttt{\mm{}external }\textit{url}~\textit{coqdir}] ~\par + + Use given URL for linking references whose name starts with prefix + \textit{coqdir}. + \item[\texttt{\mm{}coqlib }\textit{url}] ~\par Set base URL for the \Coq\ standard library (default is - \url{http://coq.inria.fr/library/}). + \url{http://coq.inria.fr/library/}). This is equivalent to + \texttt{\mm{}external }\textit{url}~\texttt{Coq}. \item[\texttt{-R }\textit{dir }\textit{coqdir}] ~\par |