File: bug5700.tex.out

package info (click to toggle)
coq-doc 8.16.1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: bookworm
  • size: 42,788 kB
  • sloc: ml: 219,673; sh: 4,035; python: 3,372; ansic: 2,529; makefile: 728; lisp: 279; javascript: 87; xml: 24; sed: 2
file content (34 lines) | stat: -rw-r--r-- 1,151 bytes parent folder | download | duplicates (4)
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
\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.bug5700}{Library }{Coqdoc.bug5700}

\begin{coqdoccode}
\end{coqdoccode}
\texttt{ foo (* \{bar\_bar\} *) } 
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
\texttt{ more (* nested (* comments *) within verbatim *) } 
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol
\end{coqdoccode}
\end{document}