1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2
% MACROS FOR THE REFERENCE MANUAL OF COQ %
3
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5
% For commentaries (define \com as {} for the release manual)
6
%\newcommand{\com}[1]{{\it(* #1 *)}}
7
%\newcommand{\com}[1]{}
10
%\renewcommand{\cuttingunit}{section}
14
\newenvironment{centerframe}%
17
\advance\dimen0 by -2\fboxrule
18
\advance\dimen0 by -2\fboxsep
20
\begin{minipage}{\dimen0}%
24
\centerline{\fbox{\box0}}\egroup
27
%HEVEA \newenvironment{centerframe}{\begin{center}}{\end{center}}
29
%HEVEA \newcommand{\vec}[1]{\mathbf{#1}}
30
%HEVEA \newcommand{\ominus}{-}
31
%HEVEA \renewcommand{\oplus}{+}
32
%HEVEA \renewcommand{\otimes}{\times}
33
%HEVEA \newcommand{\land}{\wedge}
34
%HEVEA \newcommand{\lor}{\vee}
35
%HEVEA \newcommand{\k}[1]{#1}
36
%HEVEA \newcommand{\phantom}[1]{\qquad}
38
%%%%%%%%%%%%%%%%%%%%%%%
39
% Formatting commands %
40
%%%%%%%%%%%%%%%%%%%%%%%
42
\newcommand{\ErrMsg}{\medskip \noindent {\bf Error message: }}
43
\newcommand{\ErrMsgx}{\medskip \noindent {\bf Error messages: }}
44
\newcommand{\variant}{\medskip \noindent {\bf Variant: }}
45
\newcommand{\variants}{\medskip \noindent {\bf Variants: }}
46
\newcommand{\SeeAlso}{\medskip \noindent {\bf See also: }}
47
\newcommand{\Rem}{\medskip \noindent {\bf Remark: }}
48
\newcommand{\Rems}{\medskip \noindent {\bf Remarks: }}
49
\newcommand{\Example}{\medskip \noindent {\bf Example: }}
50
\newcommand{\Warning}{\medskip \noindent {\bf Warning: }}
51
\newcommand{\Warns}{\medskip \noindent {\bf Warnings: }}
53
\newcommand{\firstexample}{\setcounter{ex}{1}}
54
\newcommand{\example}[1]{
55
\medskip \noindent \textbf{Example \arabic{ex}: }\textit{#1}
58
\newenvironment{Variant}{\variant\begin{enumerate}}{\end{enumerate}}
59
\newenvironment{Variants}{\variants\begin{enumerate}}{\end{enumerate}}
60
\newenvironment{ErrMsgs}{\ErrMsgx\begin{enumerate}}{\end{enumerate}}
61
\newenvironment{Remarks}{\Rems\begin{enumerate}}{\end{enumerate}}
62
\newenvironment{Warnings}{\Warns\begin{enumerate}}{\end{enumerate}}
63
\newenvironment{Examples}{\medskip\noindent{\bf Examples:}
64
\begin{enumerate}}{\end{enumerate}}
66
%\newcommand{\bd}{\noindent\bf}
67
%\newcommand{\sbd}{\vspace{8pt}\noindent\bf}
68
%\newcommand{\sdoll}[1]{\begin{small}$ #1~ $\end{small}}
69
%\newcommand{\sdollnb}[1]{\begin{small}$ #1 $\end{small}}
70
\newcommand{\kw}[1]{\textsf{#1}}
71
%\newcommand{\spec}[1]{\{\,#1\,\}}
73
% Building regular expressions
74
\newcommand{\zeroone}[1]{{\sl [}#1{\sl ]}}
75
%\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
76
%\newcommand{\onemany}[1]{$\{$#1$\}$+}
77
\newcommand{\nelist}[2]{{#1} {\tt #2} {\ldots} {\tt #2} {#1}}
78
\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2} {\ldots} {\tt #2} {#1}{\sl ]}}
79
\newcommand{\nelistwithoutblank}[2]{#1{\tt #2}\ldots{\tt #2}#1}
80
\newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\ldots{\tt #2}#1$]$}
83
%\newcommand{\ml}[1]{\hbox{\tt{#1}}}
84
%\newcommand{\op}{\,|\,}
86
%%%%%%%%%%%%%%%%%%%%%%%%
87
% Trademarks and so on %
88
%%%%%%%%%%%%%%%%%%%%%%%%
90
\newcommand{\Coq}{\textsc{Coq}}
91
\newcommand{\gallina}{\textsc{Gallina}}
92
\newcommand{\Gallina}{\textsc{Gallina}}
93
\newcommand{\CoqIDE}{\textsc{CoqIDE}}
94
\newcommand{\ocaml}{\textsc{Objective Caml}}
95
\newcommand{\camlpppp}{\textsc{Camlp4}}
96
\newcommand{\emacs}{\textsc{GNU Emacs}}
97
\newcommand{\CIC}{\pCIC}
98
\newcommand{\pCIC}{p\textsc{Cic}}
99
\newcommand{\iCIC}{\textsc{Cic}}
100
\newcommand{\FW}{\ensuremath{F_{\omega}}}
101
%\newcommand{\bn}{{\sf BNF}}
107
%\newcommand{\Natural}{\mbox{\tt Natural}}
113
\newcommand{\nterm}[1]{\textrm{\textsl{#1}}}
115
\newcommand{\qstring}{\nterm{string}}
117
%% New syntax specific entries
118
\newcommand{\annotation}{\nterm{annotation}}
119
\newcommand{\assums}{\nterm{assums}} % vernac
120
\newcommand{\simpleassums}{\nterm{simple\_assums}} % assumptions
121
\newcommand{\binder}{\nterm{binder}}
122
\newcommand{\binderlet}{\nterm{binderlet}}
123
\newcommand{\binderlist}{\nterm{binderlist}}
124
\newcommand{\caseitems}{\nterm{match\_items}}
125
\newcommand{\caseitem}{\nterm{match\_item}}
126
\newcommand{\eqn}{\nterm{equation}}
127
\newcommand{\ifitem}{\nterm{dep\_ret\_type}}
128
\newcommand{\letclauses}{\nterm{letclauses}}
129
\newcommand{\params}{\nterm{params}} % vernac
130
\newcommand{\returntype}{\nterm{return\_type}}
131
\newcommand{\idparams}{\nterm{ident\_with\_params}}
132
\newcommand{\statkwd}{\nterm{statement\_keyword}} % vernac
133
\newcommand{\termarg}{\nterm{arg}}
135
\newcommand{\typecstr}{\zeroone{{\tt :} {\term}}}
138
\newcommand{\Fwterm}{\textrm{\textsl{Fwterm}}}
139
\newcommand{\Index}{\textrm{\textsl{index}}}
140
\newcommand{\abbrev}{\textrm{\textsl{abbreviation}}}
141
\newcommand{\atomictac}{\textrm{\textsl{atomic\_tactic}}}
142
\newcommand{\bindinglist}{\textrm{\textsl{bindings\_list}}}
143
\newcommand{\cast}{\textrm{\textsl{cast}}}
144
\newcommand{\cofixpointbodies}{\textrm{\textsl{cofix\_bodies}}}
145
\newcommand{\cofixpointbody}{\textrm{\textsl{cofix\_body}}}
146
\newcommand{\commandtac}{\textrm{\textsl{tactic\_invocation}}}
147
\newcommand{\constructor}{\textrm{\textsl{constructor}}}
148
\newcommand{\convtactic}{\textrm{\textsl{conv\_tactic}}}
149
\newcommand{\declarationkeyword}{\textrm{\textsl{declaration\_keyword}}}
150
\newcommand{\declaration}{\textrm{\textsl{declaration}}}
151
\newcommand{\definition}{\textrm{\textsl{definition}}}
152
\newcommand{\digit}{\textrm{\textsl{digit}}}
153
\newcommand{\exteqn}{\textrm{\textsl{ext\_eqn}}}
154
\newcommand{\field}{\textrm{\textsl{field}}}
155
\newcommand{\firstletter}{\textrm{\textsl{first\_letter}}}
156
\newcommand{\fixpg}{\textrm{\textsl{fix\_pgm}}}
157
\newcommand{\fixpointbodies}{\textrm{\textsl{fix\_bodies}}}
158
\newcommand{\fixpointbody}{\textrm{\textsl{fix\_body}}}
159
\newcommand{\fixpoint}{\textrm{\textsl{fixpoint}}}
160
\newcommand{\flag}{\textrm{\textsl{flag}}}
161
\newcommand{\form}{\textrm{\textsl{form}}}
162
\newcommand{\entry}{\textrm{\textsl{entry}}}
163
\newcommand{\proditem}{\textrm{\textsl{production\_item}}}
164
\newcommand{\taclevel}{\textrm{\textsl{tactic\_level}}}
165
\newcommand{\tacargtype}{\textrm{\textsl{tactic\_argument\_type}}}
166
\newcommand{\scope}{\textrm{\textsl{scope}}}
167
\newcommand{\optscope}{\textrm{\textsl{opt\_scope}}}
168
\newcommand{\declnotation}{\textrm{\textsl{decl\_notation}}}
169
\newcommand{\symbolentry}{\textrm{\textsl{symbol}}}
170
\newcommand{\modifiers}{\textrm{\textsl{modifiers}}}
171
\newcommand{\localdef}{\textrm{\textsl{local\_def}}}
172
\newcommand{\localdecls}{\textrm{\textsl{local\_decls}}}
173
\newcommand{\ident}{\textrm{\textsl{ident}}}
174
\newcommand{\accessident}{\textrm{\textsl{access\_ident}}}
175
\newcommand{\inductivebody}{\textrm{\textsl{ind\_body}}}
176
\newcommand{\inductive}{\textrm{\textsl{inductive}}}
177
\newcommand{\naturalnumber}{\textrm{\textsl{natural}}}
178
\newcommand{\integer}{\textrm{\textsl{integer}}}
179
\newcommand{\multpattern}{\textrm{\textsl{mult\_pattern}}}
180
\newcommand{\mutualcoinductive}{\textrm{\textsl{mutual\_coinductive}}}
181
\newcommand{\mutualinductive}{\textrm{\textsl{mutual\_inductive}}}
182
\newcommand{\nestedpattern}{\textrm{\textsl{nested\_pattern}}}
183
\newcommand{\name}{\textrm{\textsl{name}}}
184
\newcommand{\num}{\textrm{\textsl{num}}}
185
\newcommand{\pattern}{\textrm{\textsl{pattern}}}
186
\newcommand{\orpattern}{\textrm{\textsl{or\_pattern}}}
187
\newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}}
188
\newcommand{\pat}{\textrm{\textsl{pat}}}
189
\newcommand{\pgs}{\textrm{\textsl{pgms}}}
190
\newcommand{\pg}{\textrm{\textsl{pgm}}}
192
\newcommand{\proof}{\textrm{\textsl{proof}}}
194
%HEVEA \renewcommand{\proof}{\textrm{\textsl{proof}}}
195
\newcommand{\record}{\textrm{\textsl{record}}}
196
\newcommand{\rewrule}{\textrm{\textsl{rewriting\_rule}}}
197
\newcommand{\sentence}{\textrm{\textsl{sentence}}}
198
\newcommand{\simplepattern}{\textrm{\textsl{simple\_pattern}}}
199
\newcommand{\sort}{\textrm{\textsl{sort}}}
200
\newcommand{\specif}{\textrm{\textsl{specif}}}
201
\newcommand{\statement}{\textrm{\textsl{statement}}}
202
\newcommand{\str}{\textrm{\textsl{string}}}
203
\newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}}
204
\newcommand{\switch}{\textrm{\textsl{switch}}}
205
\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}}
206
\newcommand{\tac}{\textrm{\textsl{tactic}}}
207
\newcommand{\terms}{\textrm{\textsl{terms}}}
208
\newcommand{\term}{\textrm{\textsl{term}}}
209
\newcommand{\module}{\textrm{\textsl{module}}}
210
\newcommand{\modexpr}{\textrm{\textsl{module\_expression}}}
211
\newcommand{\modtype}{\textrm{\textsl{module\_type}}}
212
\newcommand{\onemodbinding}{\textrm{\textsl{module\_binding}}}
213
\newcommand{\modbindings}{\textrm{\textsl{module\_bindings}}}
214
\newcommand{\qualid}{\textrm{\textsl{qualid}}}
215
\newcommand{\class}{\textrm{\textsl{class}}}
216
\newcommand{\dirpath}{\textrm{\textsl{dirpath}}}
217
\newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}}
218
\newcommand{\type}{\textrm{\textsl{type}}}
219
\newcommand{\vref}{\textrm{\textsl{ref}}}
220
\newcommand{\zarithformula}{\textrm{\textsl{zarith\_formula}}}
221
\newcommand{\zarith}{\textrm{\textsl{zarith}}}
222
\newcommand{\ltac}{\mbox{${\cal L}_{tac}$}}
224
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
225
% \mbox{\sf } series for roman text in maths formulas %
226
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
228
\newcommand{\alors}{\mbox{\textsf{then}}}
229
\newcommand{\alter}{\mbox{\textsf{alter}}}
230
\newcommand{\bool}{\mbox{\textsf{bool}}}
231
\newcommand{\conc}{\mbox{\textsf{conc}}}
232
\newcommand{\cons}{\mbox{\textsf{cons}}}
233
\newcommand{\consf}{\mbox{\textsf{consf}}}
234
\newcommand{\emptyf}{\mbox{\textsf{emptyf}}}
235
\newcommand{\EqSt}{\mbox{\textsf{EqSt}}}
236
\newcommand{\false}{\mbox{\textsf{false}}}
237
\newcommand{\filter}{\mbox{\textsf{filter}}}
238
\newcommand{\forest}{\mbox{\textsf{forest}}}
239
\newcommand{\from}{\mbox{\textsf{from}}}
240
\newcommand{\hd}{\mbox{\textsf{hd}}}
241
\newcommand{\Length}{\mbox{\textsf{Length}}}
242
\newcommand{\length}{\mbox{\textsf{length}}}
243
\newcommand{\LengthA}{\mbox {\textsf{Length\_A}}}
244
\newcommand{\List}{\mbox{\textsf{List}}}
245
\newcommand{\ListA}{\mbox{\textsf{List\_A}}}
246
\newcommand{\LNil}{\mbox{\textsf{Lnil}}}
247
\newcommand{\LCons}{\mbox{\textsf{Lcons}}}
248
\newcommand{\nat}{\mbox{\textsf{nat}}}
249
\newcommand{\nO}{\mbox{\textsf{O}}}
250
\newcommand{\nS}{\mbox{\textsf{S}}}
251
\newcommand{\node}{\mbox{\textsf{node}}}
252
\newcommand{\Nil}{\mbox{\textsf{nil}}}
253
\newcommand{\Prop}{\mbox{\textsf{Prop}}}
254
\newcommand{\Set}{\mbox{\textsf{Set}}}
255
\newcommand{\si}{\mbox{\textsf{if}}}
256
\newcommand{\sinon}{\mbox{\textsf{else}}}
257
\newcommand{\Str}{\mbox{\textsf{Stream}}}
258
\newcommand{\tl}{\mbox{\textsf{tl}}}
259
\newcommand{\tree}{\mbox{\textsf{tree}}}
260
\newcommand{\true}{\mbox{\textsf{true}}}
261
\newcommand{\Type}{\mbox{\textsf{Type}}}
262
\newcommand{\unfold}{\mbox{\textsf{unfold}}}
263
\newcommand{\zeros}{\mbox{\textsf{zeros}}}
268
\newcommand{\T}{\texttt{T}}
269
\newcommand{\U}{\texttt{U}}
270
\newcommand{\real}{\textsf{Real}}
271
\newcommand{\Spec}{\textit{Spec}}
272
\newcommand{\Data}{\textit{Data}}
273
\newcommand{\In} {{\textbf{in }}}
274
\newcommand{\AND} {{\textbf{and}}}
275
\newcommand{\If}{{\textbf{if }}}
276
\newcommand{\Else}{{\textbf{else }}}
277
\newcommand{\Then} {{\textbf{then }}}
278
\newcommand{\Let}{{\textbf{let }}}
279
\newcommand{\Where}{{\textbf{where rec }}}
280
\newcommand{\Function}{{\textbf{function }}}
281
\newcommand{\Rec}{{\textbf{rec }}}
282
%\newcommand{\cn}{\centering}
283
\newcommand{\nth}{\mbox{$^{\mbox{\scriptsize th}}$}}
285
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
286
% Math commands and symbols %
287
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
289
\newcommand{\la}{\leftarrow}
290
\newcommand{\ra}{\rightarrow}
291
\newcommand{\Ra}{\Rightarrow}
292
\newcommand{\rt}{\Rightarrow}
293
\newcommand{\lla}{\longleftarrow}
294
\newcommand{\lra}{\longrightarrow}
295
\newcommand{\Llra}{\Longleftrightarrow}
296
\newcommand{\mt}{\mapsto}
297
\newcommand{\ov}{\overrightarrow}
298
\newcommand{\wh}{\widehat}
299
\newcommand{\up}{\uparrow}
300
\newcommand{\dw}{\downarrow}
301
\newcommand{\nr}{\nearrow}
302
\newcommand{\se}{\searrow}
303
\newcommand{\sw}{\swarrow}
304
\newcommand{\nw}{\nwarrow}
307
\newcommand{\vm}[1]{\vspace{#1em}}
308
\newcommand{\vx}[1]{\vspace{#1ex}}
309
\newcommand{\hm}[1]{\hspace{#1em}}
310
\newcommand{\hx}[1]{\hspace{#1ex}}
311
\newcommand{\sm}{\mbox{ }}
312
\newcommand{\mx}{\mbox}
314
%\newcommand{\nq}{\neq}
315
%\newcommand{\eq}{\equiv}
316
\newcommand{\fa}{\forall}
317
%\newcommand{\ex}{\exists}
318
\newcommand{\impl}{\rightarrow}
319
%\newcommand{\Or}{\vee}
320
%\newcommand{\And}{\wedge}
321
\newcommand{\ms}{\models}
322
\newcommand{\bw}{\bigwedge}
323
\newcommand{\ts}{\times}
324
\newcommand{\cc}{\circ}
325
%\newcommand{\es}{\emptyset}
326
%\newcommand{\bs}{\backslash}
327
\newcommand{\vd}{\vdash}
328
%\newcommand{\lan}{{\langle }}
329
%\newcommand{\ran}{{\rangle }}
331
%\newcommand{\al}{\alpha}
332
\newcommand{\bt}{\beta}
333
%\newcommand{\io}{\iota}
334
\newcommand{\lb}{\lambda}
335
%\newcommand{\sg}{\sigma}
336
%\newcommand{\sa}{\Sigma}
337
%\newcommand{\om}{\Omega}
338
%\newcommand{\tu}{\tau}
340
%%%%%%%%%%%%%%%%%%%%%%%%%
341
% Custom maths commands %
342
%%%%%%%%%%%%%%%%%%%%%%%%%
344
\newcommand{\sumbool}[2]{\{#1\}+\{#2\}}
345
\newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3}
346
\newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2}
347
\newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}}
348
\newcommand{\WFE}[1]{\WF{E}{#1}}
349
\newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}}
350
\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
351
\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
353
\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
354
\newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\cal W\!F}(#2)}}
355
\newcommand{\WS}[3]{\ensuremath{#1[] \vdash #2 <: #3}}
356
\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
358
\newcommand{\WTRED}[5]{\mbox{$#1[#2] \vdash #3 #4 #5$}}
359
\newcommand{\WTERED}[4]{\mbox{$E[#1] \vdash #2 #3 #4$}}
360
\newcommand{\WTELECONV}[3]{\WTERED{#1}{#2}{\leconvert}{#3}}
361
\newcommand{\WTEGRED}[3]{\WTERED{\Gamma}{#1}{#2}{#3}}
362
\newcommand{\WTECONV}[3]{\WTERED{#1}{#2}{\convert}{#3}}
363
\newcommand{\WTEGCONV}[2]{\WTERED{\Gamma}{#1}{\convert}{#2}}
364
\newcommand{\WTEGLECONV}[2]{\WTERED{\Gamma}{#1}{\leconvert}{#2}}
366
\newcommand{\lab}[1]{\mathit{labels}(#1)}
367
\newcommand{\dom}[1]{\mathit{dom}(#1)}
369
\newcommand{\CI}[2]{\mbox{$\{#1\}^{#2}$}}
370
\newcommand{\CIP}[3]{\mbox{$\{#1\}_{#2}^{#3}$}}
371
\newcommand{\CIPV}[1]{\CIP{#1}{I_1.. I_k}{P_1.. P_k}}
372
\newcommand{\CIPI}[1]{\CIP{#1}{I}{P}}
373
\newcommand{\CIF}[1]{\mbox{$\{#1\}_{f_1.. f_n}$}}
375
\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(\begin{array}[t]{@{}l}#2:=#3
377
\newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{@{}l@{}}#3:=#4
380
%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}}
381
%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}}
383
\newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4
385
\newcommand{\Def}[4]{\mbox{{\sf Def}$(#1)(#2:=#3:#4)$}}
386
\newcommand{\Assum}[3]{\mbox{{\sf Assum}$(#1)(#2:#3)$}}
387
\newcommand{\Match}[3]{\mbox{$<\!#1\!>\!{\mbox{\tt Match}}~#2~{\mbox{\tt with}}~#3~{\mbox{\tt end}}$}}
388
\newcommand{\Case}[3]{\mbox{$\kw{case}(#2,#1,#3)$}}
389
\newcommand{\match}[3]{\mbox{$\kw{match}~ #2 ~\kw{with}~ #3 ~\kw{end}$}}
390
\newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}}
391
\newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}}
392
\newcommand{\With}[2]{\mbox{\tt ~with~}}
393
\newcommand{\subst}[3]{#1\{#2/#3\}}
394
\newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}}
395
\newcommand{\Sort}{\mbox{$\cal S$}}
396
\newcommand{\convert}{=_{\beta\delta\iota\zeta}}
397
\newcommand{\leconvert}{\leq_{\beta\delta\iota\zeta}}
398
\newcommand{\NN}{\mathbb{N}}
399
\newcommand{\inference}[1]{$${#1}$$}
401
\newcommand{\compat}[2]{\mbox{$[#1|#2]$}}
402
\newcommand{\tristackrel}[3]{\mathrel{\mathop{#2}\limits_{#3}^{#1}}}
404
\newcommand{\Impl}{{\it Impl}}
405
\newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}:={#3})}
406
\newcommand{\ModType}[2]{{\sf ModType}({#1}:={#2})}
407
\newcommand{\ModS}[2]{{\sf ModS}({#1}:{#2})}
408
\newcommand{\ModSEq}[3]{{\sf ModSEq}({#1}:{#2}=={#3})}
409
\newcommand{\functor}[3]{\ensuremath{{\sf Functor}(#1:#2)\;#3}}
410
\newcommand{\funsig}[3]{\ensuremath{{\sf Funsig}(#1:#2)\;#3}}
411
\newcommand{\sig}[1]{\ensuremath{{\sf Sig}~#1~{\sf End}}}
412
\newcommand{\struct}[1]{\ensuremath{{\sf Struct}~#1~{\sf End}}}
418
%\newcommand{\mud}[1]{\hfil $\displaystyle{\mathstrut #1}$\hfil}
419
%\newcommand{\rig}[1]{\hfil $\displaystyle{#1}$}
420
% \newcommand{\irulehelp}[3]{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}%
421
% \setbox\tempb=\vbox{\halign{##\cr
423
% \noalign{\vskip\the\lineskip}
424
% \noalign{\hrule height 0pt}
425
% \rig{\vbox to 0pt{\vss\hbox to 0pt{${\; #3}$\hss}\vss}}\cr
427
% \noalign{\vskip\the\lineskip}
428
% \mud{\copy\tempa}\cr}}
430
% \advance\tempc by \wd\tempa
431
% \divide\tempc by 2 }
432
% \newcommand{\irule}[3]{{\irulehelp{#1}{#2}{#3}
433
% \hbox to \wd\tempa{\hss \box\tempb \hss}}}
435
\newcommand{\sverb}[1]{{\tt #1}}
436
\newcommand{\mover}[2]{{#1\over #2}}
437
\newcommand{\jd}[2]{#1 \vdash #2}
438
\newcommand{\mathline}[1]{\[#1\]}
439
\newcommand{\zrule}[2]{#2: #1}
440
\newcommand{\orule}[3]{#3: {\mover{#1}{#2}}}
441
\newcommand{\trule}[4]{#4: \mover{#1 \qquad #2} {#3}}
442
\newcommand{\thrule}[5]{#5: {\mover{#1 \qquad #2 \qquad #3}{#4}}}
446
% placement of figures
449
\renewcommand{\topfraction}{.99}
450
\renewcommand{\bottomfraction}{.99}
451
\renewcommand{\textfraction}{.01}
452
\renewcommand{\floatpagefraction}{.9}
455
% Macros Bruno pour description de la syntaxe
457
\def\bfbar{\ensuremath{|\hskip -0.22em{}|\hskip -0.24em{}|}}
459
\def\TERMbarbar{\bfbar\bfbar}
462
%% Macros pour les grammaires
463
\def\GR#1{\text{\large(}#1\text{\large)}}
464
\def\NT#1{\langle\textit{#1}\rangle}
465
\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
466
\def\TERM#1{{\bf\textrm{\bf #1}}}
467
%\def\TERM#1{{\bf\textsf{#1}}}
468
\def\KWD#1{\TERM{#1}}
469
\def\ETERM#1{\TERM{#1}}
470
\def\CHAR#1{\TERM{#1}}
473
\def\STARGR#1{\GR{#1}*}
475
\def\PLUSGR#1{\GR{#1}+}
477
\def\OPTGR#1{\GR{#1}?}
478
%% Tableaux de definition de non-terminaux
479
\newenvironment{cadre}
480
{\begin{array}{|c|}\hline\\}
481
{\\\\\hline\end{array}}
482
\newenvironment{rulebox}
483
{$$\begin{cadre}\begin{array}{r@{~}c@{~}l@{}l@{}r}}
484
{\end{array}\end{cadre}$$}
485
\def\DEFNT#1{\NT{#1} & ::= &}
486
\def\EXTNT#1{\NT{#1} & ::= & ... \\&|&}
487
\def\RNAME#1{(\textsc{#1})}
491
\newenvironment{rules}
492
{\begin{center}\begin{rulebox}}
493
{\end{rulebox}\end{center}}
495
% $Id: macros.tex 9614 2007-02-07 18:43:42Z herbelin $
500
%%% TeX-master: "Reference-Manual"
added
removed
common/macros.tex
