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
}
|