aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq-sl.sty
blob: 9f6e5480c962bcadab700c32675ce8e88b5b3544 (plain)
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
% COQ style option, for use with the coq-latex filter.

\typeout{Document Style option `coq-sl' <7 Apr 92>.}

\ifcase\@ptsize
    \font\sltt = cmsltt10
\or \font\sltt = cmsltt10 \@halfmag
\or \font\sltt = cmsltt10 \@magscale1
\fi

{\catcode`\^^M=\active %
 \gdef\@coqinputline#1^^M{\tt Coq < #1\par} %
 \gdef\@coqoutputline#1^^M{\sltt#1\par} } %
\def\@coqblankline{\medskip}
\chardef\@coqbackslash="5C

\def\coq{
  \bgroup
  \flushleft
  \parindent 0pt
  \parskip 0pt
  \let\do\@makeother\dospecials
  \catcode`\^^M=\active
  \catcode`\\=0
  \catcode`\ \active
  \frenchspacing
  \@vobeyspaces
  \let\?\@coqinputline
  \let\:\@coqoutputline
  \let\;\@coqblankline
  \let\\\@coqbackslash
}

\def\endcoq{
  \endflushleft
  \egroup\noindent
}