1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
\documentclass[12pt]{report}
\usepackage[utf8x]{inputenc}
%Warning: tipa declares many non-standard macros used by utf8x to
%interpret utf8 characters but extra packages might have to be added
%such as "textgreek" for Greek letters not already in tipa
%or "stmaryrd" for mathematical symbols.
%Utf8 codes missing a LaTeX interpretation can be defined by using
%\DeclareUnicodeCharacter{code}{interpretation}.
%Use coqdoc's option -p to add new packages or declarations.
\usepackage{tipa}
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\usepackage{url}
\begin{document}
\coqlibrary{Coqdoc.bug12742}{Library }{Coqdoc.bug12742}
\begin{coqdoccode}
\end{coqdoccode}
Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx.
Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx
xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx. Xxxxx xxxxx
xxxx xxxx xxx xxxxx xxxxxxxxxx:
\begin{itemize}
\item \textit{Xxxxxxxxx xxxxxxx xxxxxxx} xxxxxxx ``xxxx-xxxxxx'' xxxxxxxxx:
xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx \textit{xxxx} xx
\textit{xxxxx} (xx, xxxxxxxxx, \textit{xxx'x xxxx: xxx xxx xx xxxx}).
Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx
xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx
xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx. Xxxxxxxx xx xxxx
xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx.
\item \textit{Xxxxx xxxxxxxxxx} xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx
xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx
xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx. Xxxxxx xxxx xxxxx
xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx,
xxxxx xxxx xxxxxx.
\end{itemize}
\begin{coqdoccode}
\end{coqdoccode}
\end{document}
|
