diff options
author | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-15 20:15:59 +0000 |
---|---|---|
committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-15 20:15:59 +0000 |
commit | f4469a308bd007fd70c17b980da753d6e7f070c4 (patch) | |
tree | 7066a12d3d6ac5510ca1fa1a57414392f1d09647 /doc/stdlib/Library.tex | |
parent | 730e25488e0f502359ed8c2a845b97bf0245d1e7 (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/Library.tex')
-rwxr-xr-x | doc/stdlib/Library.tex | 1 |
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} |