diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 09:26:39 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:14:40 +0100 |
| commit | ff76518771d1da2a7d3c1b1cbb8d637d2f4d7bf7 (patch) | |
| tree | b92429a1204eec37bbb22a274895ac32e0b9fc1a /doc | |
| parent | 08d6ae7520255ab846ed3ea81b48c2ae855f3ddb (diff) | |
refman/coqdoc.tex: fix two erroneous \url
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/coqdoc.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index c2591a7b9..fddee4560 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -197,8 +197,8 @@ Then invoke \texttt{coqdoc} or \texttt{coqdoc \mm{}glob-from \emph{file}} to tel Identifiers from the \Coq\ standard library are linked to the \Coq\ web site at \url{http://coq.inria.fr/library/}. This behavior can be -changed using command line options \url{--no-externals} and -\url{--coqlib}; see below. +changed using command line options \texttt{\mm{}no-externals} and +\texttt{\mm{}coqlib}; see below. \paragraph{Hiding / Showing parts of the source.} |