aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-15 20:15:59 +0000
committerGravatar gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-15 20:15:59 +0000
commitf4469a308bd007fd70c17b980da753d6e7f070c4 (patch)
tree7066a12d3d6ac5510ca1fa1a57414392f1d09647 /doc/stdlib
parent730e25488e0f502359ed8c2a845b97bf0245d1e7 (diff)
Fix failure to compile doc/stdlib/Library.tex.
Coqdoc converts the utf8 symbol lambda (that appears in Utf8_core.v) to itself when outputting utf8. Since Library.tex uses utf8x as the input encoding, it gets translated to \textlambda. This command is defined by both the LGR font encoding and the tipa package, and only by them. So the build fails. There are several solutions: 1. \usepackage[mathletters]{ucs} 2. \usepackage[T1,LGR]{fontenc} 3. \usepackage{tipa} 4. modify coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15807 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib')
-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 cb32adfcf..f410000ea 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -1,5 +1,6 @@
\documentclass[11pt]{report}
+\usepackage[mathletters]{ucs}
\usepackage[utf8x]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fullpage}