From a9630535a1bbbef0a91795a8136d67fc636a9a93 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 27 Oct 2014 10:08:56 +0100 Subject: Use the url package, since coqdoc generates \url commands. --- doc/stdlib/Library.tex | 1 + tools/coqdoc/output.ml | 1 + 2 files changed, 2 insertions(+) diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index f410000eab..44a0b1d361 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} diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 0561d9a081..67a28bfd7c 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -211,6 +211,7 @@ module Latex = struct printf "\\usepackage{fullpage}\n"; printf "\\usepackage{coqdoc}\n"; printf "\\usepackage{amsmath,amssymb}\n"; + printf "\\usepackage{url}\n"; (match !toc_depth with | None -> () | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n); -- cgit v1.2.3