← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to dev/v8-syntax/syntax-v8.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
dev/v8-syntax/syntax-v8.tex
 
1
 
 
2
\documentclass{article}
 
3
 
 
4
\usepackage{verbatim}
 
5
\usepackage{amsmath}
 
6
\usepackage{amssymb}
 
7
\usepackage{array}
 
8
\usepackage{fullpage}
 
9
 
 
10
\author{B.~Barras}
 
11
\title{Syntax of Coq V8}
 
12
 
 
13
%% Le _ est un caractère normal
 
14
\catcode`\_=13
 
15
\let\subscr=_
 
16
\def_{\ifmmode\sb\else\subscr\fi}
 
17
 
 
18
\def\bfbar{\ensuremath{|\hskip -0.22em{}|\hskip -0.24em{}|}}
 
19
\def\TERMbar{\bfbar}
 
20
\def\TERMbarbar{\bfbar\bfbar}
 
21
\def\notv{\text{_}}
 
22
\def\infx#1{\notv#1\notv}
 
23
 
 
24
 
 
25
%% Macros pour les grammaires
 
26
\def\GR#1{\text{\large(}#1\text{\large)}}
 
27
\def\NT#1{\langle\textit{#1}\rangle}
 
28
\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
 
29
\def\TERM#1{{\bf\textrm{\bf #1}}}
 
30
%\def\TERM#1{{\bf\textsf{#1}}}
 
31
\def\KWD#1{\TERM{#1}}
 
32
\def\ETERM#1{\TERM{#1}}
 
33
\def\CHAR#1{\TERM{#1}}
 
34
 
 
35
\def\STAR#1{#1*}
 
36
\def\STARGR#1{\GR{#1}*}
 
37
\def\PLUS#1{#1+}
 
38
\def\PLUSGR#1{\GR{#1}+}
 
39
\def\OPT#1{#1?}
 
40
\def\OPTGR#1{\GR{#1}?}
 
41
%% Tableaux de definition de non-terminaux
 
42
\newenvironment{cadre}
 
43
        {\begin{array}{|c|}\hline\\}
 
44
        {\\\\\hline\end{array}}
 
45
\newenvironment{rulebox}
 
46
        {$$\begin{cadre}\begin{array}{r@{~}c@{~}l@{}l@{}r}}
 
47
        {\end{array}\end{cadre}$$}
 
48
\def\DEFNT#1{\NT{#1} & ::= &}
 
49
\def\EXTNT#1{\NT{#1} & ::= & ... \\&|&}
 
50
\def\RNAME#1{(\textsc{#1})}
 
51
\def\SEPDEF{\\\\}
 
52
\def\nlsep{\\&|&}
 
53
\def\nlcont{\\&&}
 
54
\newenvironment{rules}
 
55
        {\begin{center}\begin{rulebox}}
 
56
        {\end{rulebox}\end{center}}
 
57
 
 
58
\begin{document}
 
59
 
 
60
\maketitle
 
61
 
 
62
\section{Meta notations used in this document}
 
63
 
 
64
Non-terminals are printed between angle brackets (e.g. $\NT{non-terminal}$) and
 
65
terminal symbols are printed in bold font (e.g. $\ETERM{terminal}$). Lexemes
 
66
are displayed as non-terminals.
 
67
 
 
68
The usual operators on regular expressions:
 
69
\begin{center}
 
70
\begin{tabular}{l|l}
 
71
\hfil notation & \hfil  meaning \\
 
72
\hline
 
73
$\STAR{regexp}$ & repeat $regexp$ 0 or more times \\
 
74
$\PLUS{regexp}$ & repeat $regexp$ 1 or more times \\
 
75
$\OPT{regexp}$ & $regexp$ is optional \\
 
76
$regexp_1~\mid~regexp_2$ & alternative
 
77
\end{tabular}
 
78
\end{center}
 
79
 
 
80
Parenthesis are used to group regexps. Beware to distinguish this operator
 
81
$\GR{~}$ from the terminals $\ETERM{( )}$, and $\mid$ from terminal
 
82
\TERMbar.
 
83
 
 
84
Rules are optionaly annotated in the right margin with:
 
85
\begin{itemize}
 
86
\item a precedence and associativity (L for left, R for right and N for no associativity), indicating how to solve conflicts;
 
87
  lower levels are tighter;
 
88
\item a rule name.
 
89
\end{itemize}
 
90
In order to solve some conflicts, a non-terminal may be invoked with a
 
91
precedence (notation: $\NTL{entry}{prec}$), meaning that rules with higher
 
92
precedence do not apply.
 
93
 
 
94
\section{Lexical conventions}
 
95
 
 
96
Lexical categories are:
 
97
\begin{rules}
 
98
\DEFNT{ident}
 
99
     \STARGR{\NT{letter}\mid\CHAR{_}}
 
100
     \STARGR{\NT{letter}\mid \NT{digit} \mid \CHAR{'} \mid \CHAR{_}}
 
101
\SEPDEF
 
102
\DEFNT{field}       \CHAR{.}\NT{ident}
 
103
\SEPDEF
 
104
\DEFNT{meta-ident}  \CHAR{?}\NT{ident}   
 
105
\SEPDEF
 
106
\DEFNT{num}         \PLUS{\NT{digit}}
 
107
\SEPDEF
 
108
\DEFNT{int}         \NT{num} \mid \CHAR{-}\NT{num}
 
109
\SEPDEF
 
110
\DEFNT{digit}       \CHAR{0}-\CHAR{9}
 
111
\SEPDEF
 
112
\DEFNT{letter}      \CHAR{a}-\CHAR{z}\mid\CHAR{A}-\CHAR{Z}
 
113
                    \mid\NT{unicode-letter}
 
114
 
 
115
\SEPDEF
 
116
\DEFNT{string}      \CHAR{"}~\STARGR{\CHAR{""}\mid\NT{unicode-char-but-"}}~\CHAR{"}
 
117
\end{rules}
 
118
 
 
119
Reserved identifiers for the core syntax are:
 
120
\begin{quote}
 
121
\KWD{as},
 
122
\KWD{cofix},
 
123
\KWD{else},
 
124
\KWD{end},
 
125
\KWD{fix},
 
126
\KWD{for},
 
127
\KWD{forall},
 
128
\KWD{fun},
 
129
\KWD{if},
 
130
\KWD{in},
 
131
\KWD{let},
 
132
\KWD{match}, 
 
133
\KWD{Prop},
 
134
\KWD{return}, 
 
135
\KWD{Set},
 
136
\KWD{then},
 
137
\KWD{Type},
 
138
\KWD{with}  
 
139
\end{quote}
 
140
 
 
141
Symbols used in the core syntax:
 
142
$$ \KWD{(}
 
143
~~ \KWD{)}
 
144
~~ \KWD{\{}
 
145
~~ \KWD{\}}
 
146
~~ \KWD{:}
 
147
~~ \KWD{,}
 
148
~~ \Rightarrow
 
149
~~ \rightarrow
 
150
~~ \KWD{:=}
 
151
~~ \KWD{_}
 
152
~~ \TERMbar
 
153
~~ \KWD{@}
 
154
~~ \KWD{\%}
 
155
~~ \KWD{.(}
 
156
$$
 
157
 
 
158
Note that \TERM{struct} is not a reserved identifier.
 
159
 
 
160
\section{Syntax of terms}
 
161
 
 
162
\subsection{Core syntax}
 
163
 
 
164
The main entry point of the term grammar is $\NTL{constr}{9}$. When no
 
165
conflict can appear, $\NTL{constr}{200}$ is also used as entry point.
 
166
 
 
167
\begin{rules}
 
168
\DEFNT{constr}
 
169
       \NT{binder-constr}                             &200R~~ &\RNAME{binders}
 
170
\nlsep \NT{constr}~\KWD{:}~\NT{constr}                &100R &\RNAME{cast}
 
171
\nlsep \NT{constr}~\KWD{:}~\NT{binder-constr}         &100R &\RNAME{cast'}
 
172
\nlsep \NT{constr}~\KWD{$\rightarrow$}~\NT{constr}    &80R  &\RNAME{arrow}
 
173
\nlsep \NT{constr}~\KWD{$\rightarrow$}~\NT{binder-constr} &80R &\RNAME{arrow'}
 
174
\nlsep \NT{constr}~\PLUS{\NT{appl-arg}}               &10L  &\RNAME{apply}
 
175
\nlsep \KWD{@}~\NT{reference}~\STAR{\NTL{constr}{9}}  &10L  &\RNAME{expl-apply}
 
176
\nlsep \NT{constr}~\KWD{.(}
 
177
       ~\NT{reference}~\STAR{\NT{appl-arg}}~\TERM{)}  &1L & \RNAME{proj}
 
178
\nlsep \NT{constr}~\KWD{.(}~\TERM{@}
 
179
       ~\NT{reference}~\STAR{\NTL{constr}{9}}~\TERM{)} &1L & \RNAME{expl-proj}
 
180
\nlsep \NT{constr} ~ \KWD{\%} ~ \NT{ident}            &1L   &\RNAME{scope-chg}
 
181
\nlsep \NT{atomic-constr}                             &0
 
182
\nlsep \NT{match-expr}                                &0
 
183
\nlsep \KWD{(}~\NT{constr}~\KWD{)}                    &0
 
184
\SEPDEF
 
185
\DEFNT{binder-constr}
 
186
       \KWD{forall}~\NT{binder-list}~\KWD{,}~\NTL{constr}{200} 
 
187
          &&\RNAME{prod}
 
188
\nlsep \KWD{fun} ~\NT{binder-list} ~\KWD{$\Rightarrow$}~\NTL{constr}{200}
 
189
          &&\RNAME{lambda}
 
190
\nlsep \NT{fix-expr}
 
191
\nlsep \KWD{let}~\NT{ident-with-params} ~\KWD{:=}~\NTL{constr}{200}
 
192
       ~\KWD{in}~\NTL{constr}{200}  &&\RNAME{let}
 
193
\nlsep \KWD{let}~\NT{single-fix} ~\KWD{in}~\NTL{constr}{200}
 
194
          &&\RNAME{rec-let}
 
195
\nlsep \KWD{let}~\KWD{(}~\OPT{\NT{let-pattern}}~\KWD{)}~\OPT{\NT{return-type}}
 
196
       ~\KWD{:=}~\NTL{constr}{200}~\KWD{in}~\NTL{constr}{200}
 
197
          &&\RNAME{let-case}
 
198
\nlsep \KWD{if}~\NT{if-item}
 
199
       ~\KWD{then}~\NTL{constr}{200}~\KWD{else}~\NTL{constr}{200}
 
200
          &&\RNAME{if-case}
 
201
\SEPDEF
 
202
\DEFNT{appl-arg}
 
203
       \KWD{(}~\NT{ident}~\!\KWD{:=}~\NTL{constr}{200}~\KWD{)}
 
204
          &&\RNAME{impl-arg}
 
205
\nlsep \KWD{(}~\NT{num}~\!\KWD{:=}~\NTL{constr}{200}~\KWD{)}
 
206
          &&\RNAME{impl-arg}
 
207
\nlsep \NTL{constr}{9}
 
208
\SEPDEF
 
209
\DEFNT{atomic-constr}
 
210
       \NT{reference}     && \RNAME{variables}
 
211
\nlsep \NT{sort}          && \RNAME{CIC-sort}
 
212
\nlsep \NT{num}           && \RNAME{number}
 
213
\nlsep \KWD{_}            && \RNAME{hole}
 
214
\nlsep \NT{meta-ident}    && \RNAME{meta/evar}
 
215
\end{rules}
 
216
 
 
217
 
 
218
 
 
219
\begin{rules}
 
220
\DEFNT{ident-with-params}
 
221
       \NT{ident}~\STAR{\NT{binder-let}}~\NT{type-cstr}
 
222
\SEPDEF
 
223
\DEFNT{binder-list}
 
224
       \NT{binder}~\STAR{\NT{binder-let}}
 
225
\nlsep \PLUS{\NT{name}}~\KWD{:}~\NT{constr}
 
226
\SEPDEF
 
227
\DEFNT{binder}
 
228
       \NT{name}      &&\RNAME{infer}
 
229
\nlsep \KWD{(}~\PLUS{\NT{name}}~\KWD{:}~\NT{constr}
 
230
       ~\KWD{)}      &&\RNAME{binder}
 
231
\SEPDEF
 
232
\DEFNT{binder-let}
 
233
       \NT{binder}
 
234
\nlsep \KWD{(}~\NT{name}~\NT{type-cstr}~\KWD{:=}~\NT{constr}~\KWD{)}
 
235
\SEPDEF
 
236
\DEFNT{let-pattern}
 
237
       \NT{name}
 
238
\nlsep \NT{name} ~\KWD{,} ~\NT{let-pattern}
 
239
\SEPDEF
 
240
\DEFNT{type-cstr}
 
241
       \OPTGR{\KWD{:}~\NT{constr}}
 
242
\SEPDEF
 
243
\DEFNT{reference}
 
244
       \NT{ident}                   && \RNAME{short-ident}
 
245
\nlsep \NT{ident}~\PLUS{\NT{field}} && \RNAME{qualid}
 
246
\SEPDEF
 
247
\DEFNT{sort}
 
248
       \KWD{Prop} ~\mid~ \KWD{Set} ~\mid~ \KWD{Type}
 
249
\SEPDEF
 
250
\DEFNT{name}
 
251
       \NT{ident} ~\mid~ \KWD{_}
 
252
\end{rules}
 
253
 
 
254
\begin{rules}
 
255
\DEFNT{fix-expr}
 
256
       \NT{single-fix}
 
257
\nlsep \NT{single-fix}~\PLUSGR{\KWD{with}~\NT{fix-decl}}
 
258
      ~\KWD{for}~\NT{ident}
 
259
\SEPDEF
 
260
\DEFNT{single-fix}
 
261
       \NT{fix-kw}~\NT{fix-decl}
 
262
\SEPDEF
 
263
\DEFNT{fix-kw} \KWD{fix} ~\mid~ \KWD{cofix}
 
264
\SEPDEF
 
265
\DEFNT{fix-decl}
 
266
       \NT{ident}~\STAR{\NT{binder-let}}~\OPT{\NT{annot}}~\NT{type-cstr}
 
267
       ~\KWD{:=}~\NTL{constr}{200}
 
268
\SEPDEF
 
269
\DEFNT{annot}
 
270
       \KWD{\{}~\TERM{struct}~\NT{ident}~\KWD{\}}
 
271
\end{rules}
 
272
 
 
273
 
 
274
\begin{rules}
 
275
\DEFNT{match-expr}
 
276
       \KWD{match}~\NT{match-items}~\OPT{\NT{return-type}}~\KWD{with}
 
277
  ~\OPT{\TERMbar}~\OPT{\NT{branches}}~\KWD{end}        &&\RNAME{match}
 
278
\SEPDEF
 
279
\DEFNT{match-items}
 
280
       \NT{match-item} ~\KWD{,} ~\NT{match-items}
 
281
\nlsep \NT{match-item}
 
282
\SEPDEF
 
283
\DEFNT{match-item}
 
284
       \NTL{constr}{100}~\OPTGR{\KWD{as}~\NT{name}}
 
285
       ~\OPTGR{\KWD{in}~\NTL{constr}{100}}
 
286
\SEPDEF
 
287
\DEFNT{return-type}
 
288
       \KWD{return}~\NTL{constr}{100}
 
289
\SEPDEF
 
290
\DEFNT{if-item}
 
291
       \NT{constr}~\OPTGR{\OPTGR{\KWD{as}~\NT{name}}~\NT{return-type}}
 
292
\SEPDEF
 
293
\DEFNT{branches}
 
294
       \NT{eqn}~\TERMbar~\NT{branches}
 
295
\nlsep \NT{eqn}
 
296
\SEPDEF
 
297
\DEFNT{eqn}
 
298
       \NT{pattern} ~\STARGR{\KWD{,}~\NT{pattern}}
 
299
       ~\KWD{$\Rightarrow$}~\NT{constr}
 
300
\SEPDEF
 
301
\DEFNT{pattern}
 
302
       \NT{reference}~\PLUS{\NT{pattern}}  &1L~~ & \RNAME{constructor}
 
303
\nlsep \NT{pattern}~\KWD{as}~\NT{ident}    &1L & \RNAME{alias}
 
304
\nlsep \NT{pattern}~\KWD{\%}~\NT{ident}    &1L & \RNAME{scope-change}
 
305
\nlsep \NT{reference}                      &0  & \RNAME{pattern-var}
 
306
\nlsep \KWD{_}                             &0  & \RNAME{hole}
 
307
\nlsep \NT{num}                            &0
 
308
\nlsep \KWD{(}~\NT{tuple-pattern}~\KWD{)}
 
309
\SEPDEF
 
310
\DEFNT{tuple-pattern}
 
311
       \NT{pattern}
 
312
\nlsep \NT{tuple-pattern}~\KWD{,}~\NT{pattern} && \RNAME{pair}
 
313
\end{rules}
 
314
 
 
315
\subsection{Notations of the prelude (logic and basic arithmetic)}
 
316
 
 
317
Reserved notations:
 
318
 
 
319
$$
 
320
\begin{array}{l|c}
 
321
\text{Symbol} & \text{precedence} \\
 
322
\hline
 
323
\infx{,}             & 250L \\
 
324
\KWD{IF}~\notv~\KWD{then}~\notv~\KWD{else}~\notv
 
325
                     & 200R \\
 
326
\infx{:}             & 100R \\
 
327
\infx{\leftrightarrow} & 95N \\
 
328
\infx{\rightarrow}   & 90R \\
 
329
\infx{\vee}          & 85R \\
 
330
\infx{\wedge}        & 80R \\
 
331
\tilde{}\notv        & 75R \\
 
332
\begin{array}[c]{@{}l@{}}
 
333
 \infx{=}\quad \infx{=}\KWD{$:>$}\notv \quad \infx{=}=\notv
 
334
 \quad \infx{\neq} \quad  \infx{\neq}\KWD{$:>$}\notv \\
 
335
 \infx{<}\quad\infx{>} \quad \infx{\leq}\quad\infx{\geq}
 
336
 \quad \infx{<}<\notv \quad \infx{<}\leq\notv
 
337
 \quad \infx{\leq}<\notv \quad \infx{\leq}\leq\notv
 
338
\end{array}          & 70N \\
 
339
\infx{+}\quad\infx{-}\quad -\notv   & 50L \\
 
340
\infx{*}\quad\infx{/}\quad /\notv   & 40L \\
 
341
\end{array}
 
342
$$
 
343
 
 
344
Existential quantifiers follows the \KWD{forall} notation (with same
 
345
precedence 200), but only one quantified variable is allowed.
 
346
 
 
347
\begin{rules}
 
348
\EXTNT{binder-constr}
 
349
       \NT{quantifier-kwd}~\NT{name}~\NT{type-cstr}~\KWD{,}~\NTL{constr}{200} \\
 
350
\SEPDEF
 
351
\DEFNT{quantifier-kwd}
 
352
       \TERM{exists} && \RNAME{ex}
 
353
\nlsep \TERM{exists2} && \RNAME{ex2}
 
354
\end{rules}
 
355
 
 
356
$$
 
357
\begin{array}{l|c|l}
 
358
\text{Symbol} & \text{precedence} \\
 
359
\hline
 
360
\notv+\{\notv\}                            & 50 & \RNAME{sumor} \\
 
361
\{\notv:\notv~|~\notv\}                    & 0 & \RNAME{sig} \\
 
362
\{\notv:\notv~|~\notv \& \notv \}          & 0 & \RNAME{sig2} \\
 
363
\{\notv:\notv~\&~\notv \}                  & 0 & \RNAME{sigS} \\
 
364
\{\notv:\notv~\&~\notv \& \notv \}         & 0 & \RNAME{sigS2} \\
 
365
\{\notv\}+\{\notv\}                        & 0 & \RNAME{sumbool} \\
 
366
\end{array}
 
367
$$
 
368
 
 
369
%% Strange: nat + {x:nat|x=x} * nat  == ( + ) *
 
370
 
 
371
\section{Grammar of tactics}
 
372
 
 
373
\def\tacconstr{\NTL{constr}{9}}
 
374
\def\taclconstr{\NTL{constr}{200}}
 
375
 
 
376
Additional symbols are:
 
377
$$ \TERM{'}
 
378
~~ \KWD{;}
 
379
~~ \TERM{()}
 
380
~~ \TERMbarbar
 
381
~~ \TERM{$\vdash$}
 
382
~~ \TERM{[}
 
383
~~ \TERM{]}
 
384
~~ \TERM{$\leftarrow$}
 
385
$$
 
386
Additional reserved keywords are:
 
387
$$ \KWD{at}
 
388
~~ \TERM{using}
 
389
$$
 
390
 
 
391
\subsection{Basic tactics}
 
392
 
 
393
\begin{rules}
 
394
\DEFNT{simple-tactic}
 
395
       \TERM{intros}~\TERM{until}~\NT{quantified-hyp}
 
396
\nlsep \TERM{intros}~\NT{intro-patterns}
 
397
\nlsep \TERM{intro}~\OPT{\NT{ident}}~\OPTGR{\TERM{after}~\NT{ident}}
 
398
%%
 
399
\nlsep \TERM{assumption}
 
400
\nlsep \TERM{exact}~\tacconstr
 
401
%%
 
402
\nlsep \TERM{apply}~\NT{constr-with-bindings}
 
403
\nlsep \TERM{elim}~\NT{constr-with-bindings}~\OPT{\NT{eliminator}}
 
404
\nlsep \TERM{elimtype}~\tacconstr
 
405
\nlsep \TERM{case}~\NT{constr-with-bindings}
 
406
\nlsep \TERM{casetype}~\tacconstr
 
407
\nlsep \KWD{fix}~\OPT{\NT{ident}}~\NT{num}
 
408
\nlsep \KWD{fix}~\NT{ident}~\NT{num}~\KWD{with}~\PLUS{\NT{fix-spec}}
 
409
\nlsep \KWD{cofix}~\OPT{\NT{ident}}
 
410
\nlsep \KWD{cofix}~\NT{ident}~\PLUS{\NT{fix-spec}}
 
411
%%
 
412
\nlsep \TERM{cut}~\tacconstr
 
413
\nlsep \TERM{assert}~\tacconstr
 
414
\nlsep \TERM{assert}~
 
415
  \TERM{(}~\NT{ident}~\KWD{:}~\taclconstr~\TERM{)}
 
416
\nlsep \TERM{assert}~
 
417
  \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}
 
418
\nlsep \TERM{pose}~\tacconstr
 
419
\nlsep \TERM{pose}~
 
420
  \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}
 
421
\nlsep \TERM{generalize}~\PLUS{\tacconstr}
 
422
\nlsep \TERM{generalize}~\TERM{dependent}~\tacconstr
 
423
\nlsep \TERM{set}~\tacconstr~\OPT{\NT{clause}}
 
424
\nlsep \TERM{set}~
 
425
  \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}}
 
426
\nlsep \TERM{instantiate}~
 
427
  \TERM{(}~\NT{num}~\TERM{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}}
 
428
%%
 
429
\nlsep \TERM{specialize}~\OPT{\NT{num}}~\NT{constr-with-bindings}
 
430
\nlsep \TERM{lapply}~\tacconstr
 
431
%%
 
432
\nlsep \TERM{simple}~\TERM{induction}~\NT{quantified-hyp}
 
433
\nlsep \TERM{induction}~\NT{induction-arg}~\OPT{\NT{with-names}}
 
434
       ~\OPT{\NT{eliminator}}
 
435
\nlsep \TERM{double}~\TERM{induction}~\NT{quantified-hyp}~\NT{quantified-hyp}
 
436
\nlsep \TERM{simple}~\TERM{destruct}~\NT{quantified-hyp}
 
437
\nlsep \TERM{destruct}~\NT{induction-arg}~\OPT{\NT{with-names}}
 
438
       ~\OPT{\NT{eliminator}}
 
439
\nlsep \TERM{decompose}~\TERM{record}~\tacconstr
 
440
\nlsep \TERM{decompose}~\TERM{sum}~\tacconstr
 
441
\nlsep \TERM{decompose}~\TERM{[}~\PLUS{\NT{reference}}~\TERM{]}
 
442
       ~\tacconstr
 
443
%%
 
444
\nlsep ...
 
445
\end{rules}
 
446
 
 
447
\begin{rules}
 
448
\EXTNT{simple-tactic}
 
449
       \TERM{trivial}~\OPT{\NT{hint-bases}}
 
450
\nlsep \TERM{auto}~\OPT{\NT{num}}~\OPT{\NT{hint-bases}}
 
451
%%
 
452
%%\nlsep \TERM{autotdb}~\OPT{\NT{num}}
 
453
%%\nlsep \TERM{cdhyp}~\NT{ident}
 
454
%%\nlsep \TERM{dhyp}~\NT{ident}
 
455
%%\nlsep \TERM{dconcl}
 
456
%%\nlsep \TERM{superauto}~\NT{auto-args}
 
457
\nlsep \TERM{auto}~\OPT{\NT{num}}~\TERM{decomp}~\OPT{\NT{num}}
 
458
%%
 
459
\nlsep \TERM{clear}~\PLUS{\NT{ident}}
 
460
\nlsep \TERM{clearbody}~\PLUS{\NT{ident}}
 
461
\nlsep \TERM{move}~\NT{ident}~\TERM{after}~\NT{ident}
 
462
\nlsep \TERM{rename}~\NT{ident}~\TERM{into}~\NT{ident}
 
463
%%
 
464
\nlsep \TERM{left}~\OPT{\NT{with-binding-list}}
 
465
\nlsep \TERM{right}~\OPT{\NT{with-binding-list}}
 
466
\nlsep \TERM{split}~\OPT{\NT{with-binding-list}}
 
467
\nlsep \TERM{exists}~\OPT{\NT{binding-list}}
 
468
\nlsep \TERM{constructor}~\NT{num}~\OPT{\NT{with-binding-list}}
 
469
\nlsep \TERM{constructor}~\OPT{\NT{tactic}}
 
470
%%
 
471
\nlsep \TERM{reflexivity}
 
472
\nlsep \TERM{symmetry}~\OPTGR{\KWD{in}~\NT{ident}}
 
473
\nlsep \TERM{transitivity}~\tacconstr
 
474
%%
 
475
\nlsep \NT{inversion-kwd}~\NT{quantified-hyp}~\OPT{\NT{with-names}}~\OPT{\NT{clause}}
 
476
\nlsep \TERM{dependent}~\NT{inversion-kwd}~\NT{quantified-hyp}
 
477
  ~\OPT{\NT{with-names}}~\OPTGR{\KWD{with}~\tacconstr}
 
478
\nlsep \TERM{inversion}~\NT{quantified-hyp}~\TERM{using}~\tacconstr~\OPT{\NT{clause}}
 
479
%%
 
480
\nlsep \NT{red-expr}~\OPT{\NT{clause}}
 
481
\nlsep \TERM{change}~\NT{conversion}~\OPT{\NT{clause}}
 
482
\SEPDEF
 
483
\DEFNT{red-expr}
 
484
       \TERM{red} ~\mid~ \TERM{hnf} ~\mid~ \TERM{compute}
 
485
\nlsep \TERM{simpl}~\OPT{\NT{pattern-occ}}
 
486
\nlsep \TERM{cbv}~\PLUS{\NT{red-flag}}
 
487
\nlsep \TERM{lazy}~\PLUS{\NT{red-flag}}
 
488
\nlsep \TERM{unfold}~\NT{unfold-occ}~\STARGR{\KWD{,}~\NT{unfold-occ}}
 
489
\nlsep \TERM{fold}~\PLUS{\tacconstr}
 
490
\nlsep \TERM{pattern}~\NT{pattern-occ}~\STARGR{\KWD{,}~\NT{pattern-occ}}
 
491
\SEPDEF
 
492
\DEFNT{conversion}
 
493
       \NT{pattern-occ}~\KWD{with}~\tacconstr
 
494
\nlsep \tacconstr
 
495
\SEPDEF
 
496
\DEFNT{inversion-kwd}
 
497
       \TERM{inversion} ~\mid~ \TERM{invesion_clear} ~\mid~
 
498
       \TERM{simple}~\TERM{inversion}
 
499
\end{rules}
 
500
 
 
501
Conflicts exists between integers and constrs.
 
502
 
 
503
\begin{rules}
 
504
\DEFNT{quantified-hyp}
 
505
       \NT{int}~\mid~\NT{ident}
 
506
\SEPDEF
 
507
\DEFNT{induction-arg}
 
508
       \NT{int}~\mid~\tacconstr
 
509
\SEPDEF
 
510
\DEFNT{fix-spec}
 
511
       \KWD{(}~\NT{ident}~\STAR{\NT{binder}}~\OPT{\NT{annot}}
 
512
       ~\KWD{:}~\taclconstr~\KWD{)}
 
513
\SEPDEF
 
514
\DEFNT{intro-patterns}
 
515
       \STAR{\NT{intro-pattern}}
 
516
\SEPDEF
 
517
\DEFNT{intro-pattern}
 
518
       \NT{name}
 
519
\nlsep \TERM{[}~\NT{intro-patterns}~\STARGR{\TERMbar~\NT{intro-patterns}}
 
520
       ~\TERM{]}
 
521
\nlsep \KWD{(}~\NT{intro-pattern}~\STARGR{\KWD{,}~\NT{intro-pattern}}
 
522
       ~\KWD{)}
 
523
\SEPDEF
 
524
\DEFNT{with-names}
 
525
%       \KWD{as}~\TERM{[}~\STAR{\NT{ident}}~\STARGR{\TERMbar~\STAR{\NT{ident}}}
 
526
%       ~\TERM{]}
 
527
       \KWD{as}~\NT{intro-pattern}
 
528
\SEPDEF
 
529
\DEFNT{eliminator}
 
530
       \TERM{using}~\NT{constr-with-bindings}
 
531
\SEPDEF
 
532
\DEFNT{constr-with-bindings}
 
533
       % dangling ``with'' of ``fix'' can conflict with ``with''
 
534
       \tacconstr~\OPT{\NT{with-binding-list}}
 
535
\SEPDEF
 
536
\DEFNT{with-binding-list}
 
537
       \KWD{with}~\NT{binding-list}
 
538
\SEPDEF
 
539
\DEFNT{binding-list}
 
540
       \PLUS{\tacconstr}
 
541
\nlsep \PLUS{\NT{simple-binding}}
 
542
\SEPDEF
 
543
\DEFNT{simple-binding}
 
544
       \KWD{(}~\NT{quantified-hyp}~\KWD{:=}~\taclconstr~\KWD{)}
 
545
\SEPDEF
 
546
\DEFNT{red-flag}
 
547
       \TERM{beta} ~\mid~ \TERM{iota} ~\mid~ \TERM{zeta}
 
548
       ~\mid~ \TERM{delta} ~\mid~
 
549
       \TERM{delta}~\OPT{\TERM{-}}~\TERM{[}~\PLUS{\NT{reference}}~\TERM{]}
 
550
\SEPDEF
 
551
\DEFNT{clause}
 
552
       \KWD{in}~\TERM{*}
 
553
\nlsep \KWD{in}~\TERM{*}~\KWD{$\vdash$}~\OPT{\NT{concl-occ}}
 
554
\nlsep \KWD{in}~\OPT{\NT{hyp-ident-list}} ~\KWD{$\vdash$} ~\OPT{\NT{concl-occ}}
 
555
\nlsep \KWD{in}~\OPT{\NT{hyp-ident-list}}
 
556
\SEPDEF
 
557
\DEFNT{hyp-ident-list}
 
558
       \NT{hyp-ident}
 
559
\nlsep \NT{hyp-ident}~\KWD{,}~\NT{hyp-ident-list}
 
560
\SEPDEF
 
561
\DEFNT{hyp-ident}
 
562
       \NT{ident}
 
563
\nlsep \KWD{(}~\TERM{type}~\TERM{of}~\NT{ident}~\KWD{)}
 
564
\nlsep \KWD{(}~\TERM{value}~\TERM{of}~\NT{ident}~\KWD{)}
 
565
\SEPDEF
 
566
\DEFNT{concl-occ}
 
567
       \TERM{*} ~\NT{occurrences}
 
568
\SEPDEF
 
569
\DEFNT{pattern-occ}
 
570
       \tacconstr ~\NT{occurrences}
 
571
\SEPDEF
 
572
\DEFNT{unfold-occ}
 
573
       \NT{reference}~\NT{occurrences}
 
574
\SEPDEF
 
575
\DEFNT{occurrences}
 
576
       ~\OPTGR{\KWD{at}~\PLUS{\NT{int}}}
 
577
\SEPDEF
 
578
\DEFNT{hint-bases}
 
579
       \KWD{with}~\TERM{*}
 
580
\nlsep \KWD{with}~\PLUS{\NT{ident}}
 
581
\SEPDEF
 
582
\DEFNT{auto-args}
 
583
       \OPT{\NT{num}}~\OPTGR{\TERM{adding}~\TERM{[}~\PLUS{\NT{reference}}
 
584
       ~\TERM{]}}~\OPT{\TERM{destructuring}}~\OPTGR{\TERM{using}~\TERM{tdb}}
 
585
\end{rules}
 
586
 
 
587
\subsection{Ltac}
 
588
 
 
589
%% Currently, there are conflicts with keyword \KWD{in}: in the following,
 
590
%% has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 
591
%% \begin{center}
 
592
%% \texttt{let x := simpl in ...}
 
593
%% \end{center}
 
594
 
 
595
 
 
596
\begin{rules}
 
597
\DEFNT{tactic}
 
598
       \NT{tactic} ~\KWD{;} ~\NT{tactic}  &5 &\RNAME{Then}
 
599
\nlsep \NT{tactic} ~\KWD{;}~\TERM{[} ~\OPT{\NT{tactic-seq}} ~\TERM{]}
 
600
         &5 &\RNAME{Then-seq}
 
601
%%
 
602
\nlsep \TERM{try} ~\NT{tactic}     &3R &\RNAME{Try}
 
603
\nlsep \TERM{do} ~\NT{int-or-var} ~\NT{tactic}
 
604
\nlsep \TERM{repeat} ~\NT{tactic}
 
605
\nlsep \TERM{progress} ~\NT{tactic}
 
606
\nlsep \TERM{info} ~\NT{tactic}
 
607
\nlsep \TERM{abstract}~\NTL{tactic}{2}~\OPTGR{\TERM{using}~\NT{ident}}
 
608
%%
 
609
\nlsep \NT{tactic} ~\TERMbarbar ~\NT{tactic} &2R &\RNAME{Orelse}
 
610
%%
 
611
\nlsep \KWD{fun} ~\PLUS{\NT{name}} ~\KWD{$\Rightarrow$}
 
612
       ~\NT{tactic}  &1 &\RNAME{Fun-tac}
 
613
\nlsep \KWD{let} ~\NT{let-clauses} ~\KWD{in} ~\NT{tactic}
 
614
\nlsep \KWD{let} ~\TERM{rec} ~\NT{rec-clauses} ~\KWD{in} ~\NT{tactic}
 
615
\nlsep \KWD{match}~\OPT{\TERM{reverse}}~\TERM{goal}~\KWD{with}
 
616
       ~\OPT{\TERMbar}~\OPT{\NT{match-goal-rules}} ~\KWD{end}
 
617
\nlsep \KWD{match} ~\NT{tactic} ~\KWD{with}
 
618
       ~\OPT{\TERMbar}~\OPT{\NT{match-rules}} ~\KWD{end}
 
619
\nlsep \TERM{first}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
 
620
\nlsep \TERM{solve}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
 
621
\nlsep \TERM{idtac}
 
622
\nlsep \TERM{fail} ~\OPT{\NT{num}} ~\OPT{\NT{string}}
 
623
\nlsep \TERM{constr}~\KWD{:}~\tacconstr
 
624
\nlsep \TERM{ipattern}~\KWD{:}~\NT{intro-pattern}
 
625
\nlsep \NT{term-ltac}
 
626
\nlsep \NT{reference}~\STAR{\NT{tactic-arg}}  &&\RNAME{call-tactic}
 
627
\nlsep \NT{simple-tactic}
 
628
%%
 
629
\nlsep \NT{tactic-atom}  &0 &\RNAME{atomic}
 
630
\nlsep \KWD{(} ~\NT{tactic} ~\KWD{)}
 
631
\SEPDEF
 
632
\DEFNT{tactic-arg}
 
633
       \TERM{ltac}~\KWD{:}~\NTL{tactic}{0}
 
634
\nlsep \TERM{ipattern}~\KWD{:}~\NT{intro-pattern}
 
635
\nlsep \NT{term-ltac}
 
636
\nlsep \NT{tactic-atom}
 
637
\nlsep \tacconstr
 
638
\SEPDEF
 
639
\DEFNT{term-ltac}
 
640
       \TERM{fresh} ~\OPT{\NT{string}}
 
641
\nlsep \TERM{context} ~\NT{ident} ~\TERM{[} ~\taclconstr ~\TERM{]}
 
642
\nlsep \TERM{eval} ~\NT{red-expr} ~\KWD{in} ~\tacconstr
 
643
\nlsep \TERM{type} ~\tacconstr
 
644
\SEPDEF
 
645
\DEFNT{tactic-atom}
 
646
       \NT{reference}
 
647
\nlsep \TERM{()}
 
648
\SEPDEF
 
649
\DEFNT{tactic-seq}
 
650
       \NT{tactic} ~\TERMbar ~\NT{tactic-seq}
 
651
\nlsep \NT{tactic}
 
652
\end{rules}
 
653
 
 
654
 
 
655
 
 
656
\begin{rules}
 
657
\DEFNT{let-clauses}
 
658
       \NT{let-clause} ~\STARGR{\KWD{with}~\NT{let-clause}}
 
659
\SEPDEF
 
660
\DEFNT{let-clause}
 
661
       \NT{ident} ~\STAR{\NT{name}} ~\KWD{:=} ~\NT{tactic}
 
662
\SEPDEF
 
663
\DEFNT{rec-clauses}
 
664
       \NT{rec-clause} ~\KWD{with} ~\NT{rec-clauses}
 
665
\nlsep \NT{rec-clause}
 
666
\SEPDEF
 
667
\DEFNT{rec-clause}
 
668
       \NT{ident} ~\PLUS{\NT{name}} ~\KWD{:=} ~\NT{tactic}
 
669
\SEPDEF
 
670
\DEFNT{match-goal-rules}
 
671
       \NT{match-goal-rule}
 
672
\nlsep \NT{match-goal-rule} ~\TERMbar ~\NT{match-goal-rules}
 
673
\SEPDEF
 
674
\DEFNT{match-goal-rule}
 
675
       \NT{match-hyps-list} ~\TERM{$\vdash$} ~\NT{match-pattern}
 
676
       ~\KWD{$\Rightarrow$} ~\NT{tactic}
 
677
\nlsep \KWD{[}~\NT{match-hyps-list} ~\TERM{$\vdash$} ~\NT{match-pattern}
 
678
       ~\KWD{]}~\KWD{$\Rightarrow$} ~\NT{tactic}
 
679
\nlsep \KWD{_} ~\KWD{$\Rightarrow$} ~\NT{tactic}
 
680
\SEPDEF
 
681
\DEFNT{match-hyps-list}
 
682
       \NT{match-hyps} ~\KWD{,} ~\NT{match-hyps-list}
 
683
\nlsep \NT{match-hyps}
 
684
\SEPDEF
 
685
\DEFNT{match-hyps}
 
686
       \NT{name} ~\KWD{:} ~\NT{match-pattern}
 
687
\SEPDEF
 
688
\DEFNT{match-rules}
 
689
       \NT{match-rule}
 
690
\nlsep \NT{match-rule} ~\TERMbar ~\NT{match-rules}
 
691
\SEPDEF
 
692
\DEFNT{match-rule}
 
693
       \NT{match-pattern} ~\KWD{$\Rightarrow$} ~\NT{tactic}
 
694
\nlsep \KWD{_} ~\KWD{$\Rightarrow$} ~\NT{tactic}
 
695
\SEPDEF
 
696
\DEFNT{match-pattern}
 
697
       \TERM{context}~\OPT{\NT{ident}}
 
698
       ~\TERM{[} ~\NT{constr-pattern} ~\TERM{]}  &&\RNAME{subterm}
 
699
\nlsep \NT{constr-pattern}
 
700
\SEPDEF
 
701
\DEFNT{constr-pattern}
 
702
       \tacconstr
 
703
\end{rules}
 
704
 
 
705
\subsection{Other tactics}
 
706
 
 
707
\begin{rules}
 
708
\EXTNT{simple-tactic}
 
709
       \TERM{rewrite} ~\NT{orient} ~\NT{constr-with-bindings}
 
710
         ~\OPTGR{\KWD{in}~\NT{ident}}
 
711
\nlsep \TERM{replace} ~\tacconstr ~\KWD{with} ~\tacconstr
 
712
         ~\OPTGR{\KWD{in}~\NT{ident}}
 
713
\nlsep \TERM{replace} ~\OPT{\NT{orient}} ~\tacconstr
 
714
         ~\OPTGR{\KWD{in}~\NT{ident}}
 
715
\nlsep \TERM{symplify_eq} ~\OPT{\NT{quantified-hyp}}
 
716
\nlsep \TERM{discriminate} ~\OPT{\NT{quantified-hyp}}
 
717
\nlsep \TERM{injection} ~\OPT{\NT{quantified-hyp}}
 
718
\nlsep \TERM{conditional}~\NT{tactic}~\TERM{rewrite}~\NT{orient}
 
719
         ~\NT{constr-with-bindings}~\OPTGR{\KWD{in}~\NT{ident}}
 
720
\nlsep \TERM{dependent}~\TERM{rewrite}~\NT{orient}~\NT{ident}
 
721
\nlsep \TERM{cutrewrite}~\NT{orient}~\tacconstr
 
722
         ~\OPTGR{\KWD{in}~\NT{ident}}
 
723
\nlsep \TERM{absurd} ~\tacconstr
 
724
\nlsep \TERM{contradiction}
 
725
\nlsep \TERM{autorewrite}~\NT{hint-bases}~\OPTGR{\KWD{using}~\NT{tactic}}
 
726
\nlsep \TERM{refine}~\tacconstr
 
727
\nlsep \TERM{setoid_replace} ~\tacconstr ~\KWD{with} ~\tacconstr
 
728
\nlsep \TERM{setoid_rewrite} ~\NT{orient} ~\tacconstr
 
729
\nlsep \TERM{subst} ~\STAR{\NT{ident}}
 
730
%% eqdecide.ml4
 
731
\nlsep \TERM{decide}~\TERM{equality} ~\OPTGR{\tacconstr~\tacconstr}
 
732
\nlsep \TERM{compare}~\tacconstr~\tacconstr
 
733
%% eauto
 
734
\nlsep \TERM{eexact}~\tacconstr
 
735
\nlsep \TERM{eapply}~\NT{constr-with-bindings}
 
736
\nlsep \TERM{prolog}~\TERM{[}~\STAR{\tacconstr}~\TERM{]}
 
737
         ~\NT{quantified-hyp}
 
738
\nlsep \TERM{eauto}~\OPT{\NT{quantified-hyp}}~\OPT{\NT{quantified-hyp}}
 
739
         ~\NT{hint-bases}
 
740
\nlsep \TERM{eautod}~\OPT{\NT{quantified-hyp}}~\OPT{\NT{quantified-hyp}}
 
741
         ~\NT{hint-bases}
 
742
%% tauto
 
743
\nlsep \TERM{tauto}
 
744
\nlsep \TERM{simplif}
 
745
\nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}}
 
746
\nlsep \TERM{linearintuition}~\OPT{\NT{num}}
 
747
%% contrib/cc
 
748
\nlsep \TERM{cc}
 
749
%% contrib/field
 
750
\nlsep \TERM{field}~\STAR{\tacconstr}
 
751
%% contrib/firstorder
 
752
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
 
753
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
 
754
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
 
755
%%\nlsep \TERM{gtauto}
 
756
\nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
 
757
%% contrib/fourier
 
758
\nlsep \TERM{fourierZ}
 
759
%% contrib/funind
 
760
\nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr}
 
761
%% contrib/jprover
 
762
\nlsep \TERM{jp}~\OPT{\NT{num}}
 
763
%% contrib/omega
 
764
\nlsep \TERM{omega}
 
765
%% contrib/ring
 
766
\nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
 
767
\nlsep \TERM{ring}~\STAR{\tacconstr}
 
768
%% contrib/romega
 
769
\nlsep \TERM{romega}
 
770
\SEPDEF
 
771
\DEFNT{orient}
 
772
       \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$}
 
773
\end{rules}
 
774
 
 
775
\section{Grammar of commands}
 
776
 
 
777
New symbols:
 
778
$$ \TERM{.}
 
779
~~ \TERM{..}
 
780
~~ \TERM{\tt >->}
 
781
~~ \TERM{:$>$}
 
782
~~ \TERM{$<$:}
 
783
$$
 
784
 
 
785
New keyword:
 
786
$$ \KWD{where}
 
787
$$
 
788
 
 
789
\subsection{Classification of commands}
 
790
 
 
791
\begin{rules}
 
792
\DEFNT{vernac}
 
793
       \TERM{Time}~\NT{vernac}  &2~~ &\RNAME{Timing}
 
794
%%
 
795
\nlsep \NT{gallina}~\TERM{.}    &1
 
796
\nlsep \NT{command}~\TERM{.}
 
797
\nlsep \NT{syntax}~\TERM{.}
 
798
\nlsep \TERM{[}~\PLUS{\NT{vernac}}~\TERM{]}~\TERM{.}
 
799
%%
 
800
\nlsep \OPTGR{\NT{num}~\KWD{:}}~\NT{subgoal-command}~\TERM{.} ~~~&0
 
801
\SEPDEF
 
802
\DEFNT{subgoal-command}
 
803
       \NT{check-command}
 
804
\nlsep %\OPT{\TERM{By}}~
 
805
   \NT{tactic}~\OPT{\KWD{..}}
 
806
\end{rules}
 
807
 
 
808
\subsection{Gallina and extensions}
 
809
 
 
810
\begin{rules}
 
811
\DEFNT{gallina}
 
812
       \NT{thm-token}~\NT{ident}~\STAR{\NT{binder-let}}~\KWD{:}~\NT{constr}
 
813
\nlsep \NT{def-token}~\NT{ident}~\NT{def-body}
 
814
\nlsep \NT{assum-token}~\NT{assum-list}
 
815
\nlsep \NT{finite-token}~\NT{inductive-definition}
 
816
      ~\STARGR{\KWD{with}~\NT{inductive-definition}}
 
817
\nlsep \TERM{Fixpoint}~\NT{fix-decl}~\STARGR{\KWD{with}~\NT{fix-decl}}
 
818
\nlsep \TERM{CoFixpoint}~\NT{fix-decl}~\STARGR{\KWD{with}~\NT{fix-decl}}
 
819
\nlsep \TERM{Scheme}~\NT{scheme}~\STARGR{\KWD{with}~\NT{scheme}}
 
820
%% Extension: record
 
821
\nlsep \NT{record-tok}~\OPT{\TERM{$>$}}~\NT{ident}~\STAR{\NT{binder-let}}
 
822
       ~\KWD{:}~\NT{constr}~\KWD{:=}
 
823
       ~\OPT{\NT{ident}}~\KWD{\{}~\NT{field-list}~\KWD{\}}
 
824
\nlsep \TERM{Ltac}~\NT{ltac-def}~\STARGR{~\TERM{with}~\NT{ltac-def}}
 
825
\end{rules}
 
826
 
 
827
\begin{rules}
 
828
\DEFNT{thm-token}
 
829
   \TERM{Theorem} ~\mid~ \TERM{Lemma} ~\mid~ \TERM{Fact} ~\mid~ \TERM{Remark}
 
830
\SEPDEF
 
831
\DEFNT{def-token}
 
832
   \TERM{Definition} ~\mid~ \TERM{Let} ~\mid~
 
833
   \OPT{\TERM{Local}}~\TERM{SubClass}
 
834
\SEPDEF
 
835
\DEFNT{assum-token}
 
836
    \TERM{Hypothesis} ~\mid~ \TERM{Variable} ~\mid~ \TERM{Axiom} ~\mid~
 
837
    \TERM{Parameter}
 
838
\SEPDEF
 
839
\DEFNT{finite-token}
 
840
    \TERM{Inductive} ~\mid~ \TERM{CoInductive}
 
841
\SEPDEF
 
842
\DEFNT{record-tok}
 
843
    \TERM{Record} ~\mid~ \TERM{Structure}
 
844
\end{rules}
 
845
 
 
846
 
 
847
\begin{rules}
 
848
\DEFNT{def-body}
 
849
       \STAR{\NT{binder-let}}~\NT{type-cstr}~\KWD{:=}
 
850
       ~\OPT{\NT{reduce}}~\NT{constr}
 
851
\nlsep \STAR{\NT{binder-let}}~\KWD{:}~\NT{constr}
 
852
\SEPDEF
 
853
\DEFNT{reduce}
 
854
       \TERM{Eval}~\NT{red-expr}~\KWD{in}
 
855
\SEPDEF
 
856
\DEFNT{ltac-def}
 
857
       \NT{ident}~\STAR{\NT{name}}~\KWD{:=}~\NT{tactic}
 
858
\SEPDEF
 
859
\DEFNT{rec-definition}
 
860
       \NT{fix-decl}~\OPT{\NT{decl-notation}}
 
861
\SEPDEF
 
862
\DEFNT{inductive-definition}
 
863
       \OPT{\NT{string}}~\NT{ident}~\STAR{\NT{binder-let}}~\KWD{:}
 
864
       ~\NT{constr}~\KWD{:=}
 
865
       ~\OPT{\TERMbar}~\OPT{\NT{constructor-list}}
 
866
       ~\OPT{\NT{decl-notation}}
 
867
\SEPDEF
 
868
\DEFNT{constructor-list}
 
869
       \NT{constructor}~\TERMbar~\NT{constructor-list}
 
870
\nlsep \NT{constructor}
 
871
\SEPDEF
 
872
\DEFNT{constructor}
 
873
       \NT{ident}~\STAR{\NT{binder-let}}\OPTGR{\NT{coerce-kwd}~\NT{constr}}
 
874
\SEPDEF
 
875
\DEFNT{decl-notation}
 
876
       \TERM{where}~\NT{string}~\TERM{:=}~\NT{constr}
 
877
\SEPDEF
 
878
\DEFNT{field-list}
 
879
       \NT{field}~\KWD{;}~\NT{field-list}
 
880
\nlsep \NT{field}
 
881
\SEPDEF
 
882
\DEFNT{field}
 
883
       \NT{ident}~\OPTGR{\NT{coerce-kwd}~\NT{constr}}
 
884
\nlsep \NT{ident}~\NT{type-cstr-coe}~\KWD{:=}~\NT{constr}
 
885
\SEPDEF
 
886
\DEFNT{assum-list}
 
887
       \PLUS{\GR{\KWD{(}~\NT{simple-assum-coe}~\KWD{)}}}
 
888
\nlsep \NT{simple-assum-coe}
 
889
\SEPDEF
 
890
\DEFNT{simple-assum-coe}
 
891
       \PLUS{\NT{ident}}~\NT{coerce-kwd}~\NT{constr}
 
892
\SEPDEF
 
893
\DEFNT{coerce-kwd} \TERM{:$>$} ~\mid~ \KWD{:}
 
894
\SEPDEF
 
895
\DEFNT{type-cstr-coe} \OPTGR{\NT{coerce-kwd}~\NT{constr}}
 
896
\SEPDEF
 
897
\DEFNT{scheme}
 
898
       \NT{ident}~\KWD{:=}~\NT{dep-scheme}~\KWD{for}~\NT{reference}
 
899
       ~\TERM{Sort}~\NT{sort}
 
900
\SEPDEF
 
901
\DEFNT{dep-scheme}
 
902
       \TERM{Induction}~\mid~\TERM{Minimality}
 
903
\end{rules}
 
904
 
 
905
\subsection{Modules and sections}
 
906
 
 
907
\begin{rules}
 
908
\DEFNT{gallina}
 
909
       \TERM{Module}~\NT{ident}~\STAR{\NT{mbinder}}~\OPT{\NT{of-mod-type}}
 
910
       ~\OPTGR{\KWD{:=}~\NT{mod-expr}}
 
911
\nlsep \TERM{Module}~\KWD{Type}~\NT{ident}~\STAR{\NT{mbinder}}
 
912
       ~\OPTGR{\KWD{:=}~\NT{mod-type}}
 
913
\nlsep \TERM{Declare}~\TERM{Module}~\NT{ident}~\STAR{\NT{mbinder}}
 
914
       ~\OPT{\NT{of-mod-type}}
 
915
       ~\OPTGR{\KWD{:=}~\NT{mod-expr}}
 
916
\nlsep \TERM{Section}~\NT{ident}
 
917
\nlsep \TERM{Chapter}~\NT{ident}
 
918
\nlsep \TERM{End}~\NT{ident}
 
919
%%
 
920
\nlsep \TERM{Require}~\OPT{\NT{export-token}}~\OPT{\NT{specif-token}}
 
921
       ~\PLUS{\NT{reference}}
 
922
\nlsep \TERM{Require}~\OPT{\NT{export-token}}~\OPT{\NT{specif-token}}
 
923
       ~\NT{string}
 
924
\nlsep \TERM{Import}~\PLUS{\NT{reference}}
 
925
\nlsep \TERM{Export}~\PLUS{\NT{reference}}
 
926
\SEPDEF
 
927
\DEFNT{export-token}
 
928
       \TERM{Import} ~\mid~ \TERM{Export}
 
929
\SEPDEF
 
930
\DEFNT{specif-token}
 
931
       \TERM{Implementation} ~\mid~ \TERM{Specification}
 
932
\SEPDEF
 
933
\DEFNT{mod-expr}
 
934
       \NT{reference}
 
935
\nlsep \NT{mod-expr}~\NT{mod-expr} & L
 
936
\nlsep \KWD{(}~\NT{mod-expr}~\KWD{)}
 
937
\SEPDEF
 
938
\DEFNT{mod-type}
 
939
       \NT{reference}
 
940
\nlsep \NT{mod-type}~\KWD{with}~\NT{with-declaration}
 
941
\SEPDEF
 
942
\DEFNT{with-declaration}
 
943
                                                          %on forcera les ( )
 
944
                                                          %si exceptionnellemt
 
945
                                                          %un fixpoint ici
 
946
       \TERM{Definition}~\NT{ident}~\KWD{:=}~\NTL{constr}{} %{100}
 
947
\nlsep \TERM{Module}~\NT{ident}~\KWD{:=}~\NT{reference}
 
948
\SEPDEF
 
949
\DEFNT{of-mod-type}
 
950
       \KWD{:}~\NT{mod-type}
 
951
\nlsep \TERM{$<$:}~\NT{mod-type}
 
952
\SEPDEF
 
953
\DEFNT{mbinder}
 
954
       \KWD{(}~\PLUS{\NT{ident}}~\KWD{:}~\NT{mod-type}~\KWD{)}
 
955
\end{rules}
 
956
 
 
957
\begin{rules}
 
958
\DEFNT{gallina}
 
959
       \TERM{Transparent}~\PLUS{\NT{reference}}
 
960
\nlsep \TERM{Opaque}~\PLUS{\NT{reference}}
 
961
\nlsep \TERM{Canonical}~\TERM{Structure}~\NT{reference}~\OPT{\NT{def-body}}
 
962
\nlsep \TERM{Coercion}~\OPT{\TERM{Local}}~\NT{reference}~\NT{def-body}
 
963
\nlsep \TERM{Coercion}~\OPT{\TERM{Local}}~\NT{reference}~\KWD{:}
 
964
       ~\NT{class-rawexpr}~\TERM{$>->$}~\NT{class-rawexpr}
 
965
\nlsep \TERM{Identity}~\TERM{Coercion}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:}
 
966
       ~\NT{class-rawexpr}~\TERM{$>->$}~\NT{class-rawexpr}
 
967
\nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}~\TERM{[}~\STAR{\NT{num}}~\TERM{]}
 
968
\nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}
 
969
\nlsep \TERM{Implicit}~\KWD{Type}~\PLUS{\NT{ident}}~\KWD{:}~\NT{constr}
 
970
\SEPDEF
 
971
\DEFNT{command}
 
972
       \TERM{Comments}~\STAR{\NT{comment}}
 
973
\nlsep \TERM{Pwd}
 
974
\nlsep \TERM{Cd}~\OPT{\NT{string}}
 
975
\nlsep \TERM{Drop} ~\mid~ \TERM{ProtectedLoop} ~\mid~\TERM{Quit}
 
976
%%
 
977
\nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{ident}
 
978
\nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{string}
 
979
\nlsep \TERM{Declare}~\TERM{ML}~\TERM{Module}~\PLUS{\NT{string}}
 
980
\nlsep \TERM{Dump}~\TERM{Universes}~\OPT{\NT{string}}
 
981
\nlsep \TERM{Locate}~\NT{locatable}
 
982
\nlsep \TERM{Add}~\OPT{\TERM{Rec}}~\TERM{LoadPath}~\NT{string}~\OPT{\NT{as-dirpath}}
 
983
\nlsep \TERM{Remove}~\TERM{LoadPath}~\NT{string}
 
984
\nlsep \TERM{Add}~\OPT{\TERM{Rec}}~\TERM{ML}~\TERM{Path}~\NT{string}
 
985
%%
 
986
\nlsep \KWD{Type}~\NT{constr}
 
987
\nlsep \TERM{Print}~\NT{printable}
 
988
\nlsep \TERM{Print}~\NT{reference}
 
989
\nlsep \TERM{Inspect}~\NT{num}
 
990
\nlsep \TERM{About}~\NT{reference}
 
991
%%
 
992
\nlsep \TERM{Search}~\NT{reference}~\OPT{\NT{in-out-modules}}
 
993
\nlsep \TERM{SearchPattern}~\NT{constr-pattern}~\OPT{\NT{in-out-modules}}
 
994
\nlsep \TERM{SearchRewrite}~\NT{constr-pattern}~\OPT{\NT{in-out-modules}}
 
995
\nlsep \TERM{SearchAbout}~\NT{reference}~\OPT{\NT{in-out-modules}}
 
996
\nlsep \TERM{SearchAbout}~\TERM{[}~\STAR{\NT{ref-or-string}}~\TERM{]}\OPT{\NT{in-out-modules}}
 
997
\nlsep \KWD{Set}~\NT{ident}~\OPT{\NT{opt-value}}
 
998
\nlsep \TERM{Unset}~\NT{ident}
 
999
\nlsep \KWD{Set}~\NT{ident}~\NT{ident}~\OPT{\NT{opt-value}}
 
1000
\nlsep \KWD{Set}~\NT{ident}~\NT{ident}~\PLUS{\NT{opt-ref-value}}
 
1001
\nlsep \TERM{Unset}~\NT{ident}~\NT{ident}~\STAR{\NT{opt-ref-value}}
 
1002
%%
 
1003
\nlsep \TERM{Print}~\TERM{Table}~\NT{ident}~\NT{ident}
 
1004
\nlsep \TERM{Print}~\TERM{Table}~\NT{ident}
 
1005
\nlsep \TERM{Add}~\NT{ident}~\OPT{\NT{ident}}~\PLUS{\NT{opt-ref-value}}
 
1006
%%
 
1007
\nlsep \TERM{Test}~\NT{ident}~\OPT{\NT{ident}}~\STAR{\NT{opt-ref-value}}
 
1008
%%
 
1009
\nlsep \TERM{Remove}~\NT{ident}~\OPT{\NT{ident}}~\PLUS{\NT{opt-ref-value}}
 
1010
\SEPDEF
 
1011
\DEFNT{check-command}
 
1012
       \TERM{Eval}~\NT{red-expr}~\KWD{in}~\NT{constr}
 
1013
\nlsep \TERM{Check}~\NT{constr}
 
1014
\SEPDEF
 
1015
\DEFNT{ref-or-string}
 
1016
       \NT{reference}
 
1017
\nlsep \NT{string}
 
1018
\end{rules}
 
1019
 
 
1020
\begin{rules}
 
1021
\DEFNT{printable}
 
1022
       \TERM{Term}~\NT{reference}
 
1023
\nlsep \TERM{All}
 
1024
\nlsep \TERM{Section}~\NT{reference}
 
1025
\nlsep \TERM{Grammar}~\NT{ident}
 
1026
\nlsep \TERM{LoadPath}
 
1027
\nlsep \TERM{Module}~\OPT{\KWD{Type}}~\NT{reference}
 
1028
\nlsep \TERM{Modules}
 
1029
\nlsep \TERM{ML}~\TERM{Path}
 
1030
\nlsep \TERM{ML}~\TERM{Modules}
 
1031
\nlsep \TERM{Graph}
 
1032
\nlsep \TERM{Classes}
 
1033
\nlsep \TERM{Coercions}
 
1034
\nlsep \TERM{Coercion}~\TERM{Paths}~\NT{class-rawexpr}~\NT{class-rawexpr}
 
1035
\nlsep \TERM{Tables}
 
1036
% \nlsep \TERM{Proof}~\NT{reference}  % Obsolete, useful in V6.3 ??
 
1037
\nlsep \TERM{Hint}~\OPT{\NT{reference}}
 
1038
\nlsep \TERM{Hint}~\TERM{*}
 
1039
\nlsep \TERM{HintDb}~\NT{ident}
 
1040
\nlsep \TERM{Scopes}
 
1041
\nlsep \TERM{Scope}~\NT{ident}
 
1042
\nlsep \TERM{Visibility}~\OPT{\NT{ident}}
 
1043
\nlsep \TERM{Implicit}~\NT{reference}
 
1044
\SEPDEF
 
1045
\DEFNT{class-rawexpr}
 
1046
       \TERM{Funclass}~\mid~\TERM{Sortclass}~\mid~\NT{reference}
 
1047
\SEPDEF
 
1048
\DEFNT{locatable}
 
1049
       \NT{reference}
 
1050
\nlsep \TERM{File}~\NT{string}
 
1051
\nlsep \TERM{Library}~\NT{reference}
 
1052
\nlsep \NT{string}
 
1053
\SEPDEF
 
1054
\DEFNT{opt-value}
 
1055
       \NT{ident} ~\mid~ \NT{string}
 
1056
\SEPDEF
 
1057
\DEFNT{opt-ref-value}
 
1058
       \NT{reference} ~\mid~ \NT{string}
 
1059
\SEPDEF
 
1060
\DEFNT{as-dirpath}
 
1061
       \KWD{as}~\NT{reference}
 
1062
\SEPDEF
 
1063
\DEFNT{in-out-modules}
 
1064
       \TERM{inside}~\PLUS{\NT{reference}}
 
1065
\nlsep \TERM{outside}~\PLUS{\NT{reference}}
 
1066
\SEPDEF
 
1067
\DEFNT{comment}
 
1068
       \NT{constr}
 
1069
\nlsep \NT{string}
 
1070
\end{rules}
 
1071
 
 
1072
\subsection{Other commands}
 
1073
 
 
1074
%% TODO: min/maj pas a jour
 
1075
\begin{rules}
 
1076
\EXTNT{command}
 
1077
       \TERM{Debug}~\TERM{On}
 
1078
\nlsep \TERM{Debug}~\TERM{Off}
 
1079
%% TODO: vernac
 
1080
\nlsep \TERM{Add}~\TERM{setoid}~\tacconstr~\tacconstr~\tacconstr
 
1081
\nlsep \TERM{Add}~\TERM{morphism}~\tacconstr~\KWD{:}~\NT{ident}
 
1082
\nlsep \TERM{Derive}~\TERM{inversion_clear}
 
1083
         ~\OPT{\NT{num}}~\NT{ident}~\NT{ident}
 
1084
\nlsep \TERM{Derive}~\TERM{inversion_clear}
 
1085
         ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
 
1086
\nlsep \TERM{Derive}~\TERM{inversion}
 
1087
         ~\OPT{\NT{num}}~\NT{ident}~\NT{ident}
 
1088
\nlsep \TERM{Derive}~\TERM{inversion}
 
1089
         ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
 
1090
\nlsep \TERM{Derive}~\TERM{dependent}~\TERM{inversion_clear}
 
1091
         ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
 
1092
\nlsep \TERM{Derive}~\TERM{dependent}~\TERM{inversion}
 
1093
         ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
 
1094
%% Correctness: obsolete ?
 
1095
%\nlsep Correctness
 
1096
%\nlsep Global Variable
 
1097
%% TODO: extraction
 
1098
\nlsep Extraction ...
 
1099
%% field
 
1100
\nlsep \TERM{Add}~\TERM{Field}~\tacconstr~\tacconstr~\tacconstr
 
1101
         ~\tacconstr~\tacconstr~\tacconstr
 
1102
\nlcont~~~~\tacconstr~\tacconstr~\OPT{\NT{minus-div}}
 
1103
%% funind
 
1104
\nlsep \TERM{Functional}~\TERM{Scheme}~\NT{ident}~\KWD{:=}
 
1105
         ~\TERM{Induction}~\KWD{for}~\tacconstr
 
1106
         ~\OPTGR{\KWD{with}~\PLUS{\tacconstr}}
 
1107
%% ring
 
1108
\nlsep \TERM{Add}~\TERM{Ring}~\tacconstr~\tacconstr~\tacconstr
 
1109
         ~\tacconstr~\tacconstr~\tacconstr
 
1110
\nlcont~~~~\tacconstr~\tacconstr~\KWD{[}~\PLUS{\tacconstr}~\KWD{]}
 
1111
\nlsep \TERM{Add}~\TERM{Semi}~\TERM{Ring}~\tacconstr~\tacconstr~\tacconstr
 
1112
         ~\tacconstr~\tacconstr~\tacconstr
 
1113
\nlcont~~~~\tacconstr~\KWD{[}~\PLUS{\tacconstr}~\KWD{]}
 
1114
\nlsep \TERM{Add}~\TERM{Abstract}~\TERM{Ring}~\tacconstr~\tacconstr~\tacconstr
 
1115
         ~\tacconstr~\tacconstr~\tacconstr
 
1116
\nlcont~~~~\tacconstr~\tacconstr
 
1117
\nlsep \TERM{Add}~\TERM{Abstract}~\TERM{Semi}~\TERM{Ring}~\tacconstr
 
1118
         ~\tacconstr~\tacconstr~\tacconstr~\tacconstr~\tacconstr
 
1119
\nlcont~~~~\tacconstr
 
1120
\nlsep \TERM{Add}~\TERM{Setoid}~\TERM{Ring}~\tacconstr~\tacconstr~\tacconstr
 
1121
         ~\tacconstr~\tacconstr~\tacconstr
 
1122
\nlcont~~~~\tacconstr~\tacconstr~\tacconstr~\tacconstr~\tacconstr~\tacconstr
 
1123
         ~\tacconstr~\KWD{[}~\PLUS{\tacconstr}~\KWD{]}
 
1124
\nlsep \TERM{Add}~\TERM{Setoid}~\TERM{Semi}~\TERM{Ring}~\tacconstr~\tacconstr
 
1125
         ~\tacconstr~\tacconstr~\tacconstr~\tacconstr
 
1126
\nlcont~~~~\tacconstr~\tacconstr~\tacconstr~\tacconstr~\tacconstr
 
1127
         ~\KWD{[}~\PLUS{tacconstr}~\KWD{]}
 
1128
\SEPDEF
 
1129
\DEFNT{minus-div}
 
1130
       \KWD{with}~\NT{minus-arg}~\NT{div-arg}
 
1131
\nlsep \KWD{with}~\NT{div-arg}~\NT{minus-arg}
 
1132
\SEPDEF
 
1133
\DEFNT{minus-arg}
 
1134
       \TERM{minus}~\KWD{:=}~\tacconstr
 
1135
\SEPDEF
 
1136
\DEFNT{div-arg}
 
1137
       \TERM{div}~\KWD{:=}~\tacconstr
 
1138
\end{rules}
 
1139
 
 
1140
\begin{rules}
 
1141
\EXTNT{command}
 
1142
       \TERM{Write}~\TERM{State}~\NT{ident}
 
1143
\nlsep \TERM{Write}~\TERM{State}~\NT{string}
 
1144
\nlsep \TERM{Restore}~\TERM{State}~\NT{ident}
 
1145
\nlsep \TERM{Restore}~\TERM{State}~\NT{string}
 
1146
\nlsep \TERM{Reset}~\NT{ident}
 
1147
\nlsep \TERM{Reset}~\TERM{Initial}
 
1148
\nlsep \TERM{Back}~\OPT{\NT{num}}
 
1149
\end{rules}
 
1150
 
 
1151
\subsection{Proof-editing commands}
 
1152
 
 
1153
\begin{rules}
 
1154
\EXTNT{command}
 
1155
       \TERM{Goal}~\NT{constr}
 
1156
\nlsep \TERM{Proof}~\OPT{\NT{constr}}
 
1157
\nlsep \TERM{Proof}~\KWD{with}~\NT{tactic}
 
1158
\nlsep \TERM{Abort}~\OPT{\TERM{All}}
 
1159
\nlsep \TERM{Abort}~\NT{ident}
 
1160
\nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
 
1161
\nlsep \TERM{Qed}
 
1162
\nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}}
 
1163
\nlsep \TERM{Defined}~\OPT{\NT{ident}}
 
1164
\nlsep \TERM{Suspend}
 
1165
\nlsep \TERM{Resume}~\OPT{\NT{ident}}
 
1166
\nlsep \TERM{Restart}
 
1167
\nlsep \TERM{Undo}~\OPT{\NT{num}}
 
1168
\nlsep \TERM{Focus}~\OPT{\NT{num}}
 
1169
\nlsep \TERM{Unfocus}
 
1170
\nlsep \TERM{Show}~\OPT{\NT{num}}
 
1171
\nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}}
 
1172
\nlsep \TERM{Show}~\TERM{Node}
 
1173
\nlsep \TERM{Show}~\TERM{Script}
 
1174
\nlsep \TERM{Show}~\TERM{Existentials}
 
1175
\nlsep \TERM{Show}~\TERM{Tree}
 
1176
\nlsep \TERM{Show}~\TERM{Conjecture}
 
1177
\nlsep \TERM{Show}~\TERM{Proof}
 
1178
\nlsep \TERM{Show}~\TERM{Intro}
 
1179
\nlsep \TERM{Show}~\TERM{Intros}
 
1180
%% Correctness: obsolete ?
 
1181
%%\nlsep \TERM{Show}~\TERM{Programs}
 
1182
\nlsep \TERM{Explain}~\TERM{Proof}~\OPT{\TERM{Tree}}~\STAR{\NT{num}}
 
1183
%% Go not documented
 
1184
\nlsep \TERM{Hint}~\OPT{\TERM{Local}}~\NT{hint}~\OPT{\NT{inbases}}
 
1185
%% PrintConstr not documented
 
1186
\end{rules}
 
1187
 
 
1188
 
 
1189
\begin{rules}
 
1190
\DEFNT{constr-body}
 
1191
       \NT{type-cstr}~\KWD{:=}~\NT{constr}
 
1192
\SEPDEF
 
1193
\DEFNT{hint}
 
1194
       \TERM{Resolve}~\PLUS{\NTL{constr}{9}}
 
1195
\nlsep \TERM{Immediate}~\PLUS{\NTL{constr}{9}}
 
1196
\nlsep \TERM{Unfold}~\PLUS{\NT{reference}}
 
1197
\nlsep \TERM{Constructors}~\PLUS{\NT{reference}}
 
1198
\nlsep \TERM{Extern}~\NT{num}~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
 
1199
\nlsep \TERM{Destruct}~\NT{ident}~\KWD{:=}~\NT{num}~\NT{destruct-loc}
 
1200
       ~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
 
1201
\nlsep \TERM{Rewrite}~\NT{orient}~\PLUS{\NTL{constr}{9}}
 
1202
       ~\OPTGR{\KWD{using}~\NT{tactic}}
 
1203
\SEPDEF
 
1204
\DEFNT{inbases}
 
1205
       \KWD{:}~\PLUS{\NT{ident}}
 
1206
\SEPDEF
 
1207
\DEFNT{destruct-loc}
 
1208
       \TERM{Conclusion}
 
1209
\nlsep \OPT{\TERM{Discardable}}~\TERM{Hypothesis}
 
1210
\end{rules}
 
1211
 
 
1212
 
 
1213
\subsection{Syntax extensions}
 
1214
 
 
1215
\begin{rules}
 
1216
\DEFNT{syntax}
 
1217
       \TERM{Open}~\TERM{Scope}~\NT{ident}
 
1218
\nlsep \TERM{Close}~\TERM{Scope}~\NT{ident}
 
1219
\nlsep \TERM{Delimit}~\TERM{Scope}~\NT{ident}~\KWD{with}~\NT{ident}
 
1220
\nlsep \TERM{Bind}~\TERM{Scope}~\NT{ident}~\KWD{with}~\PLUS{\NT{class-rawexpr}}
 
1221
\nlsep \TERM{Arguments}~\TERM{Scope}~\NT{reference}
 
1222
       ~\TERM{[}~\PLUS{\NT{name}}~\TERM{]}
 
1223
\nlsep \TERM{Infix}~\OPT{\TERM{Local}} %%% ~\NT{prec}~\OPT{\NT{num}}
 
1224
       ~\NT{string}~\KWD{:=}~\NT{reference}~\OPT{\NT{modifiers}}
 
1225
       ~\OPT{\NT{in-scope}}
 
1226
\nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{string}~\KWD{:=}~\NT{constr}
 
1227
       ~\OPT{\NT{modifiers}}~\OPT{\NT{in-scope}}
 
1228
\nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:=}~\NT{constr}
 
1229
       ~\OPT{\KWD{(}\TERM{only~\TERM{parsing}\KWD{)}}}
 
1230
\nlsep \TERM{Reserved}~\TERM{Notation}~\OPT{\TERM{Local}}~\NT{string}
 
1231
       ~\OPT{\NT{modifiers}}
 
1232
\nlsep \TERM{Tactic}~\TERM{Notation}~\NT{string}~\STAR{\NT{tac-production}}
 
1233
       ~\KWD{:=}~\NT{tactic}
 
1234
\SEPDEF
 
1235
\DEFNT{modifiers}
 
1236
       \KWD{(}~\NT{mod-list}~\KWD{)}
 
1237
\SEPDEF
 
1238
\DEFNT{mod-list}
 
1239
       \NT{modifier}
 
1240
\nlsep \NT{modifier}~\KWD{,}~\NT{mod-list}
 
1241
\SEPDEF
 
1242
\DEFNT{modifier}
 
1243
       \NT{ident}~\KWD{at}~\NT{num}
 
1244
\nlsep \NT{ident}~\STARGR{\KWD{,}~\NT{ident}}~\KWD{at}~\NT{num}
 
1245
\nlsep \KWD{at}~\TERM{next}~\TERM{level}
 
1246
\nlsep \KWD{at}~\TERM{level}~\NT{num}
 
1247
\nlsep \TERM{left}~\TERM{associativity}
 
1248
\nlsep \TERM{right}~\TERM{associativity}
 
1249
\nlsep \TERM{no}~\TERM{associativity}
 
1250
\nlsep \NT{ident}~\NT{syntax-entry}
 
1251
\nlsep \TERM{only}~\TERM{parsing}
 
1252
\nlsep \TERM{format}~\NT{string}
 
1253
\SEPDEF
 
1254
\DEFNT{in-scope}
 
1255
       \KWD{:}~\NT{ident}
 
1256
\SEPDEF
 
1257
\DEFNT{syntax-entry}
 
1258
       \TERM{ident}~\mid~\TERM{global}~\mid~\TERM{bigint}
 
1259
\SEPDEF
 
1260
\DEFNT{tac-production}
 
1261
       \NT{string}
 
1262
\nlsep \NT{ident}~\TERM{(}~\NT{ident}~\TERM{)}
 
1263
%%% \SEPDEF
 
1264
%%% \DEFNT{prec}
 
1265
%%%       \TERM{LeftA}~\mid~\TERM{RightA}~\mid~\TERM{NonA}
 
1266
\end{rules}
 
1267
 
 
1268
\end{document}