diff options
| -rw-r--r-- | doc/Reference-Manual.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index 8eb7f3eb08..c32d053682 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -5,9 +5,10 @@ \fi \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} -\usepackage{pslatex} +\usepackage{times} \usepackage{url} \usepackage{verbatim} +\usepackage{amssymb} % for coqide \ifx\pdfoutput\undefined % si on est pas en pdflatex @@ -25,7 +26,7 @@ \input{./headers.tex}% extension .tex pour htmlgen \begin{document} -\sloppy\hbadness=3500 +\sloppy\hbadness=5000 \tophtml{} \coverpage{Reference Manual}{The Coq Development Team} |