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') 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} -- cgit v1.2.3