aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-10-27 10:08:56 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-10-27 10:32:11 +0100
commita9630535a1bbbef0a91795a8136d67fc636a9a93 (patch)
treed5cda6c13ab4345497e6c52241f01f1e7461075f /doc
parent4249ab5cac5bb0d638400b14c389ded98b3c8ea8 (diff)
Use the url package, since coqdoc generates \url commands.
Diffstat (limited to 'doc')
-rwxr-xr-xdoc/stdlib/Library.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index f410000ea..44a0b1d36 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -5,6 +5,7 @@
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{amsfonts}
+\usepackage{url}
\usepackage[color]{../../coqdoc}
\input{../common/version}