From f4469a308bd007fd70c17b980da753d6e7f070c4 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Sat, 15 Sep 2012 20:15:59 +0000
Subject: 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
---
 doc/stdlib/Library.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/stdlib/Library.tex')

diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index cb32adfcfd..f410000eab 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}
-- 
cgit v1.2.3

