diff options
| -rw-r--r-- | doc/faq/FAQ.tex | 4 | ||||
| -rwxr-xr-x | doc/stdlib/Library.tex | 1 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 2 | ||||
| -rw-r--r-- | tools/coqdoc/cdglobals.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 1 |
5 files changed, 6 insertions, 4 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index baf3d4991..0e5b00d37 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1688,7 +1688,7 @@ Lemma Rwf : well_founded R. \item Define the step function (which needs proofs that recursive calls are on smaller arguments). -\begin{coq_example*} +\begin{verbatim} Definition split (l : list nat) : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l} := (* ... *) . @@ -1698,7 +1698,7 @@ Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) let (l1,H1) := lH1 in let (l2,H2) := lH2 in concat (f l1 H1) (f l2 H2). -\end{coq_example*} +\end{verbatim} \item Define the recursive function by fixpoint on the step function. diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 02dc61bfe..cb32adfcf 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,6 +3,7 @@ \usepackage[utf8x]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} +\usepackage{amsfonts} \usepackage[color]{../../coqdoc} \input{../common/version} diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index d82e205a6..cea2e3195 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -273,7 +273,7 @@ Module Make (W0:CyclicType) <: NType. lazy beta iota delta [iter_sym dom_op dom_t comparen_m]. reflexivity. Qed. -(** TODO: no need for ZnZ.Spec_rect , _ind, and so on... *) +(** TODO: no need for ZnZ.Spec_rect , Spec_ind, and so on... *) Theorem spec_compare : forall x y, compare x y = Zcompare [x] [y]. diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 63ea264bf..cfe86a276 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -87,7 +87,7 @@ let set_latin1 () = let set_utf8 () = charset := "utf-8"; - inputenc := "utf8"; + inputenc := "utf8x"; utf8 := true (* Parsing options *) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 1052a98a9..938ecfb63 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -182,6 +182,7 @@ module Latex = struct if !header_trailer then begin printf "\\documentclass[12pt]{report}\n"; if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc; + if !inputenc = "utf8x" then printf "\\usepackage{tipa}\n"; printf "\\usepackage[T1]{fontenc}\n"; printf "\\usepackage{fullpage}\n"; printf "\\usepackage{coqdoc}\n"; |