\documentclass{article}

\usepackage{verbatim}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{array}
\usepackage{fullpage}

\author{B.~Barras}
\title{Syntax of Coq V8}

%% Le _ est un caractère normal
\catcode`\_=13
\let\subscr=_
\def_{\ifmmode\sb\else\subscr\fi}

\def\bfbar{\ensuremath{|\hskip -0.22em{}|\hskip -0.24em{}|}}
\def\TERMbar{\bfbar}
\def\TERMbarbar{\bfbar\bfbar}
\def\notv{\text{_}}
\def\infx#1{\notv#1\notv}


%% Macros pour les grammaires
\def\GR#1{\text{\large(}#1\text{\large)}}
\def\NT#1{\langle\textit{#1}\rangle}
\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
\def\TERM#1{{\bf\textrm{\bf #1}}}
%\def\TERM#1{{\bf\textsf{#1}}}
\def\KWD#1{\TERM{#1}}
\def\ETERM#1{\TERM{#1}}
\def\CHAR#1{\TERM{#1}}

\def\STAR#1{#1*}
\def\STARGR#1{\GR{#1}*}
\def\PLUS#1{#1+}
\def\PLUSGR#1{\GR{#1}+}
\def\OPT#1{#1?}
\def\OPTGR#1{\GR{#1}?}
%% Tableaux de definition de non-terminaux
\newenvironment{cadre}
        {\begin{array}{|c|}\hline\\}
        {\\\\\hline\end{array}}
\newenvironment{rulebox}
        {$$\begin{cadre}\begin{array}{r@{~}c@{~}l@{}l@{}r}}
        {\end{array}\end{cadre}$$}
\def\DEFNT#1{\NT{#1} & ::= &}
\def\EXTNT#1{\NT{#1} & ::= & ... \\&|&}
\def\RNAME#1{(\textsc{#1})}
\def\SEPDEF{\\\\}
\def\nlsep{\\&|&}
\def\nlcont{\\&&}
\newenvironment{rules}
        {\begin{center}\begin{rulebox}}
        {\end{rulebox}\end{center}}

\begin{document}

\maketitle

\section{Meta notations used in this document}

Non-terminals are printed between angle brackets (e.g. $\NT{non-terminal}$) and
terminal symbols are printed in bold font (e.g. $\ETERM{terminal}$). Lexemes
are displayed as non-terminals.

The usual operators on regular expressions:
\begin{center}
\begin{tabular}{l|l}
\hfil notation & \hfil  meaning \\
\hline
$\STAR{regexp}$ & repeat $regexp$ 0 or more times \\
$\PLUS{regexp}$ & repeat $regexp$ 1 or more times \\
$\OPT{regexp}$ & $regexp$ is optional \\
$regexp_1~\mid~regexp_2$ & alternative
\end{tabular}
\end{center}

Parenthesis are used to group regexps. Beware to distinguish this operator
$\GR{~}$ from the terminals $\ETERM{( )}$, and $\mid$ from terminal
\TERMbar.

Rules are optionally annotated in the right margin with:
\begin{itemize}
\item a precedence and associativity (L for left, R for right and N for no associativity), indicating how to solve conflicts;
  lower levels are tighter;
\item a rule name.
\end{itemize}
In order to solve some conflicts, a non-terminal may be invoked with a
precedence (notation: $\NTL{entry}{prec}$), meaning that rules with higher
precedence do not apply.

\section{Lexical conventions}

Lexical categories are:
\begin{rules}
\DEFNT{ident}
     \STARGR{\NT{letter}\mid\CHAR{_}}
     \STARGR{\NT{letter}\mid \NT{digit} \mid \CHAR{'} \mid \CHAR{_}}
\SEPDEF
\DEFNT{field}       \CHAR{.}\NT{ident}
\SEPDEF
\DEFNT{meta-ident}  \CHAR{?}\NT{ident}   
\SEPDEF
\DEFNT{num}         \PLUS{\NT{digit}}
\SEPDEF
\DEFNT{int}         \NT{num} \mid \CHAR{-}\NT{num}
\SEPDEF
\DEFNT{digit}       \CHAR{0}-\CHAR{9}
\SEPDEF
\DEFNT{letter}      \CHAR{a}-\CHAR{z}\mid\CHAR{A}-\CHAR{Z}
                    \mid\NT{unicode-letter}

\SEPDEF
\DEFNT{string}      \CHAR{"}~\STARGR{\CHAR{""}\mid\NT{unicode-char-but-"}}~\CHAR{"}
\end{rules}

Reserved identifiers for the core syntax are:
\begin{quote}
\KWD{as},
\KWD{cofix},
\KWD{else},
\KWD{end},
\KWD{fix},
\KWD{for},
\KWD{forall},
\KWD{fun},
\KWD{if},
\KWD{in},
\KWD{let},
\KWD{match}, 
\KWD{Prop},
\KWD{return}, 
\KWD{Set},
\KWD{then},
\KWD{Type},
\KWD{with}  
\end{quote}

Symbols used in the core syntax:
$$ \KWD{(}
~~ \KWD{)}
~~ \KWD{\{}
~~ \KWD{\}}
~~ \KWD{:}
~~ \KWD{,}
~~ \Rightarrow
~~ \rightarrow
~~ \KWD{:=}
~~ \KWD{_}
~~ \TERMbar
~~ \KWD{@}
~~ \KWD{\%}
~~ \KWD{.(}
$$

Note that \TERM{struct} is not a reserved identifier.

\section{Syntax of terms}

\subsection{Core syntax}

The main entry point of the term grammar is $\NTL{constr}{9}$. When no
conflict can appear, $\NTL{constr}{200}$ is also used as entry point.

\begin{rules}
\DEFNT{constr}
       \NT{binder-constr}                             &200R~~ &\RNAME{binders}
\nlsep \NT{constr}~\KWD{:}~\NT{constr}                &100R &\RNAME{cast}
\nlsep \NT{constr}~\KWD{:}~\NT{binder-constr}         &100R &\RNAME{cast'}
\nlsep \NT{constr}~\KWD{$\rightarrow$}~\NT{constr}    &80R  &\RNAME{arrow}
\nlsep \NT{constr}~\KWD{$\rightarrow$}~\NT{binder-constr} &80R &\RNAME{arrow'}
\nlsep \NT{constr}~\PLUS{\NT{appl-arg}}               &10L  &\RNAME{apply}
\nlsep \KWD{@}~\NT{reference}~\STAR{\NTL{constr}{9}}  &10L  &\RNAME{expl-apply}
\nlsep \NT{constr}~\KWD{.(}
       ~\NT{reference}~\STAR{\NT{appl-arg}}~\TERM{)}  &1L & \RNAME{proj}
\nlsep \NT{constr}~\KWD{.(}~\TERM{@}
       ~\NT{reference}~\STAR{\NTL{constr}{9}}~\TERM{)} &1L & \RNAME{expl-proj}
\nlsep \NT{constr} ~ \KWD{\%} ~ \NT{ident}            &1L   &\RNAME{scope-chg}
\nlsep \NT{atomic-constr}                             &0
\nlsep \NT{match-expr}                                &0
\nlsep \KWD{(}~\NT{constr}~\KWD{)}                    &0
\SEPDEF
\DEFNT{binder-constr}
       \KWD{forall}~\NT{binder-list}~\KWD{,}~\NTL{constr}{200} 
          &&\RNAME{prod}
\nlsep \KWD{fun} ~\NT{binder-list} ~\KWD{$\Rightarrow$}~\NTL{constr}{200}
          &&\RNAME{lambda}
\nlsep \NT{fix-expr}
\nlsep \KWD{let}~\NT{ident-with-params} ~\KWD{:=}~\NTL{constr}{200}
       ~\KWD{in}~\NTL{constr}{200}  &&\RNAME{let}
\nlsep \KWD{let}~\NT{single-fix} ~\KWD{in}~\NTL{constr}{200}
          &&\RNAME{rec-let}
\nlsep \KWD{let}~\KWD{(}~\OPT{\NT{let-pattern}}~\KWD{)}~\OPT{\NT{return-type}}
       ~\KWD{:=}~\NTL{constr}{200}~\KWD{in}~\NTL{constr}{200}
          &&\RNAME{let-case}
\nlsep \KWD{if}~\NT{if-item}
       ~\KWD{then}~\NTL{constr}{200}~\KWD{else}~\NTL{constr}{200}
          &&\RNAME{if-case}
\SEPDEF
\DEFNT{appl-arg}
       \KWD{(}~\NT{ident}~\!\KWD{:=}~\NTL{constr}{200}~\KWD{)}
          &&\RNAME{impl-arg}
\nlsep \KWD{(}~\NT{num}~\!\KWD{:=}~\NTL{constr}{200}~\KWD{)}
          &&\RNAME{impl-arg}
\nlsep \NTL{constr}{9}
\SEPDEF
\DEFNT{atomic-constr}
       \NT{reference}     && \RNAME{variables}
\nlsep \NT{sort}          && \RNAME{CIC-sort}
\nlsep \NT{num}           && \RNAME{number}
\nlsep \KWD{_}            && \RNAME{hole}
\nlsep \NT{meta-ident}    && \RNAME{meta/evar}
\end{rules}



\begin{rules}
\DEFNT{ident-with-params}
       \NT{ident}~\STAR{\NT{binder-let}}~\NT{type-cstr}
\SEPDEF
\DEFNT{binder-list}
       \NT{binder}~\STAR{\NT{binder-let}}
\nlsep \PLUS{\NT{name}}~\KWD{:}~\NT{constr}
\SEPDEF
\DEFNT{binder}
       \NT{name}      &&\RNAME{infer}
\nlsep \KWD{(}~\PLUS{\NT{name}}~\KWD{:}~\NT{constr}
       ~\KWD{)}      &&\RNAME{binder}
\SEPDEF
\DEFNT{binder-let}
       \NT{binder}
\nlsep \KWD{(}~\NT{name}~\NT{type-cstr}~\KWD{:=}~\NT{constr}~\KWD{)}
\SEPDEF
\DEFNT{let-pattern}
       \NT{name}
\nlsep \NT{name} ~\KWD{,} ~\NT{let-pattern}
\SEPDEF
\DEFNT{type-cstr}
       \OPTGR{\KWD{:}~\NT{constr}}
\SEPDEF
\DEFNT{reference}
       \NT{ident}                   && \RNAME{short-ident}
\nlsep \NT{ident}~\PLUS{\NT{field}} && \RNAME{qualid}
\SEPDEF
\DEFNT{sort}
       \KWD{Prop} ~\mid~ \KWD{Set} ~\mid~ \KWD{Type}
\SEPDEF
\DEFNT{name}
       \NT{ident} ~\mid~ \KWD{_}
\end{rules}

\begin{rules}
\DEFNT{fix-expr}
       \NT{single-fix}
\nlsep \NT{single-fix}~\PLUSGR{\KWD{with}~\NT{fix-decl}}
      ~\KWD{for}~\NT{ident}
\SEPDEF
\DEFNT{single-fix}
       \NT{fix-kw}~\NT{fix-decl}
\SEPDEF
\DEFNT{fix-kw} \KWD{fix} ~\mid~ \KWD{cofix}
\SEPDEF
\DEFNT{fix-decl}
       \NT{ident}~\STAR{\NT{binder-let}}~\OPT{\NT{annot}}~\NT{type-cstr}
       ~\KWD{:=}~\NTL{constr}{200}
\SEPDEF
\DEFNT{annot}
       \KWD{\{}~\TERM{struct}~\NT{ident}~\KWD{\}}
\end{rules}


\begin{rules}
\DEFNT{match-expr}
       \KWD{match}~\NT{match-items}~\OPT{\NT{return-type}}~\KWD{with}
  ~\OPT{\TERMbar}~\OPT{\NT{branches}}~\KWD{end}        &&\RNAME{match}
\SEPDEF
\DEFNT{match-items}
       \NT{match-item} ~\KWD{,} ~\NT{match-items}
\nlsep \NT{match-item}
\SEPDEF
\DEFNT{match-item}
       \NTL{constr}{100}~\OPTGR{\KWD{as}~\NT{name}}
       ~\OPTGR{\KWD{in}~\NTL{constr}{100}}
\SEPDEF
\DEFNT{return-type}
       \KWD{return}~\NTL{constr}{100}
\SEPDEF
\DEFNT{if-item}
       \NT{constr}~\OPTGR{\OPTGR{\KWD{as}~\NT{name}}~\NT{return-type}}
\SEPDEF
\DEFNT{branches}
       \NT{eqn}~\TERMbar~\NT{branches}
\nlsep \NT{eqn}
\SEPDEF
\DEFNT{eqn}
       \NT{pattern} ~\STARGR{\KWD{,}~\NT{pattern}}
       ~\KWD{$\Rightarrow$}~\NT{constr}
\SEPDEF
\DEFNT{pattern}
       \NT{reference}~\PLUS{\NT{pattern}}  &1L~~ & \RNAME{constructor}
\nlsep \NT{pattern}~\KWD{as}~\NT{ident}    &1L & \RNAME{alias}
\nlsep \NT{pattern}~\KWD{\%}~\NT{ident}    &1L & \RNAME{scope-change}
\nlsep \NT{reference}                      &0  & \RNAME{pattern-var}
\nlsep \KWD{_}                             &0  & \RNAME{hole}
\nlsep \NT{num}                            &0
\nlsep \KWD{(}~\NT{tuple-pattern}~\KWD{)}
\SEPDEF
\DEFNT{tuple-pattern}
       \NT{pattern}
\nlsep \NT{tuple-pattern}~\KWD{,}~\NT{pattern} && \RNAME{pair}
\end{rules}

\subsection{Notations of the prelude (logic and basic arithmetic)}

Reserved notations:

$$
\begin{array}{l|c}
\text{Symbol} & \text{precedence} \\
\hline
\infx{,}             & 250L \\
\KWD{IF}~\notv~\KWD{then}~\notv~\KWD{else}~\notv
                     & 200R \\
\infx{:}             & 100R \\
\infx{\leftrightarrow} & 95N \\
\infx{\rightarrow}   & 90R \\
\infx{\vee}          & 85R \\
\infx{\wedge}        & 80R \\
\tilde{}\notv        & 75R \\
\begin{array}[c]{@{}l@{}}
 \infx{=}\quad \infx{=}\KWD{$:>$}\notv \quad \infx{=}=\notv
 \quad \infx{\neq} \quad  \infx{\neq}\KWD{$:>$}\notv \\
 \infx{<}\quad\infx{>} \quad \infx{\leq}\quad\infx{\geq}
 \quad \infx{<}<\notv \quad \infx{<}\leq\notv
 \quad \infx{\leq}<\notv \quad \infx{\leq}\leq\notv
\end{array}          & 70N \\
\infx{+}\quad\infx{-}\quad -\notv   & 50L \\
\infx{*}\quad\infx{/}\quad /\notv   & 40L \\
\end{array}
$$

Existential quantifiers follows the \KWD{forall} notation (with same
precedence 200), but only one quantified variable is allowed.

\begin{rules}
\EXTNT{binder-constr}
       \NT{quantifier-kwd}~\NT{name}~\NT{type-cstr}~\KWD{,}~\NTL{constr}{200} \\
\SEPDEF
\DEFNT{quantifier-kwd}
       \TERM{exists} && \RNAME{ex}
\nlsep \TERM{exists2} && \RNAME{ex2}
\end{rules}

$$
\begin{array}{l|c|l}
\text{Symbol} & \text{precedence} \\
\hline
\notv+\{\notv\}                            & 50 & \RNAME{sumor} \\
\{\notv:\notv~|~\notv\}                    & 0 & \RNAME{sig} \\
\{\notv:\notv~|~\notv \& \notv \}          & 0 & \RNAME{sig2} \\
\{\notv:\notv~\&~\notv \}                  & 0 & \RNAME{sigS} \\
\{\notv:\notv~\&~\notv \& \notv \}         & 0 & \RNAME{sigS2} \\
\{\notv\}+\{\notv\}                        & 0 & \RNAME{sumbool} \\
\end{array}
$$

%% Strange: nat + {x:nat|x=x} * nat  == ( + ) *

\section{Grammar of tactics}

\def\tacconstr{\NTL{constr}{9}}
\def\taclconstr{\NTL{constr}{200}}

Additional symbols are:
$$ \TERM{'}
~~ \KWD{;}
~~ \TERM{()}
~~ \TERMbarbar
~~ \TERM{$\vdash$}
~~ \TERM{[}
~~ \TERM{]}
~~ \TERM{$\leftarrow$}
$$
Additional reserved keywords are:
$$ \KWD{at}
~~ \TERM{using}
$$

\subsection{Basic tactics}

\begin{rules}
\DEFNT{simple-tactic}
       \TERM{intros}~\TERM{until}~\NT{quantified-hyp}
\nlsep \TERM{intros}~\NT{intro-patterns}
\nlsep \TERM{intro}~\OPT{\NT{ident}}~\OPTGR{\TERM{after}~\NT{ident}}
%%
\nlsep \TERM{assumption}
\nlsep \TERM{exact}~\tacconstr
%%
\nlsep \TERM{apply}~\NT{constr-with-bindings}
\nlsep \TERM{elim}~\NT{constr-with-bindings}~\OPT{\NT{eliminator}}
\nlsep \TERM{elimtype}~\tacconstr
\nlsep \TERM{case}~\NT{constr-with-bindings}
\nlsep \TERM{casetype}~\tacconstr
\nlsep \KWD{fix}~\OPT{\NT{ident}}~\NT{num}
\nlsep \KWD{fix}~\NT{ident}~\NT{num}~\KWD{with}~\PLUS{\NT{fix-spec}}
\nlsep \KWD{cofix}~\OPT{\NT{ident}}
\nlsep \KWD{cofix}~\NT{ident}~\PLUS{\NT{fix-spec}}
%%
\nlsep \TERM{cut}~\tacconstr
\nlsep \TERM{assert}~\tacconstr
\nlsep \TERM{assert}~
  \TERM{(}~\NT{ident}~\KWD{:}~\taclconstr~\TERM{)}
\nlsep \TERM{assert}~
  \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}
\nlsep \TERM{pose}~\tacconstr
\nlsep \TERM{pose}~
  \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}
\nlsep \TERM{generalize}~\PLUS{\tacconstr}
\nlsep \TERM{generalize}~\TERM{dependent}~\tacconstr
\nlsep \TERM{set}~\tacconstr~\OPT{\NT{clause}}
\nlsep \TERM{set}~
  \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}}
\nlsep \TERM{instantiate}~
  \TERM{(}~\NT{num}~\TERM{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}}
%%
\nlsep \TERM{specialize}~\OPT{\NT{num}}~\NT{constr-with-bindings}
\nlsep \TERM{lapply}~\tacconstr
%%
\nlsep \TERM{simple}~\TERM{induction}~\NT{quantified-hyp}
\nlsep \TERM{induction}~\NT{induction-arg}~\OPT{\NT{with-names}}
       ~\OPT{\NT{eliminator}}
\nlsep \TERM{double}~\TERM{induction}~\NT{quantified-hyp}~\NT{quantified-hyp}
\nlsep \TERM{simple}~\TERM{destruct}~\NT{quantified-hyp}
\nlsep \TERM{destruct}~\NT{induction-arg}~\OPT{\NT{with-names}}
       ~\OPT{\NT{eliminator}}
\nlsep \TERM{decompose}~\TERM{record}~\tacconstr
\nlsep \TERM{decompose}~\TERM{sum}~\tacconstr
\nlsep \TERM{decompose}~\TERM{[}~\PLUS{\NT{reference}}~\TERM{]}
       ~\tacconstr
%%
\nlsep ...
\end{rules}

\begin{rules}
\EXTNT{simple-tactic}
       \TERM{trivial}~\OPT{\NT{hint-bases}}
\nlsep \TERM{auto}~\OPT{\NT{num}}~\OPT{\NT{hint-bases}}
%%
%%\nlsep \TERM{autotdb}~\OPT{\NT{num}}
%%\nlsep \TERM{cdhyp}~\NT{ident}
%%\nlsep \TERM{dhyp}~\NT{ident}
%%\nlsep \TERM{dconcl}
%%\nlsep \TERM{superauto}~\NT{auto-args}
\nlsep \TERM{auto}~\OPT{\NT{num}}~\TERM{decomp}~\OPT{\NT{num}}
%%
\nlsep \TERM{clear}~\PLUS{\NT{ident}}
\nlsep \TERM{clearbody}~\PLUS{\NT{ident}}
\nlsep \TERM{move}~\NT{ident}~\TERM{after}~\NT{ident}
\nlsep \TERM{rename}~\NT{ident}~\TERM{into}~\NT{ident}
%%
\nlsep \TERM{left}~\OPT{\NT{with-binding-list}}
\nlsep \TERM{right}~\OPT{\NT{with-binding-list}}
\nlsep \TERM{split}~\OPT{\NT{with-binding-list}}
\nlsep \TERM{exists}~\OPT{\NT{binding-list}}
\nlsep \TERM{constructor}~\NT{num}~\OPT{\NT{with-binding-list}}
\nlsep \TERM{constructor}~\OPT{\NT{tactic}}
%%
\nlsep \TERM{reflexivity}
\nlsep \TERM{symmetry}~\OPTGR{\KWD{in}~\NT{ident}}
\nlsep \TERM{transitivity}~\tacconstr
%%
\nlsep \NT{inversion-kwd}~\NT{quantified-hyp}~\OPT{\NT{with-names}}~\OPT{\NT{clause}}
\nlsep \TERM{dependent}~\NT{inversion-kwd}~\NT{quantified-hyp}
  ~\OPT{\NT{with-names}}~\OPTGR{\KWD{with}~\tacconstr}
\nlsep \TERM{inversion}~\NT{quantified-hyp}~\TERM{using}~\tacconstr~\OPT{\NT{clause}}
%%
\nlsep \NT{red-expr}~\OPT{\NT{clause}}
\nlsep \TERM{change}~\NT{conversion}~\OPT{\NT{clause}}
\SEPDEF
\DEFNT{red-expr}
       \TERM{red} ~\mid~ \TERM{hnf} ~\mid~ \TERM{compute}
\nlsep \TERM{simpl}~\OPT{\NT{pattern-occ}}
\nlsep \TERM{cbv}~\PLUS{\NT{red-flag}}
\nlsep \TERM{lazy}~\PLUS{\NT{red-flag}}
\nlsep \TERM{unfold}~\NT{unfold-occ}~\STARGR{\KWD{,}~\NT{unfold-occ}}
\nlsep \TERM{fold}~\PLUS{\tacconstr}
\nlsep \TERM{pattern}~\NT{pattern-occ}~\STARGR{\KWD{,}~\NT{pattern-occ}}
\SEPDEF
\DEFNT{conversion}
       \NT{pattern-occ}~\KWD{with}~\tacconstr
\nlsep \tacconstr
\SEPDEF
\DEFNT{inversion-kwd}
       \TERM{inversion} ~\mid~ \TERM{invesion_clear} ~\mid~
       \TERM{simple}~\TERM{inversion}
\end{rules}

Conflicts exists between integers and constrs.

\begin{rules}
\DEFNT{quantified-hyp}
       \NT{int}~\mid~\NT{ident}
\SEPDEF
\DEFNT{induction-arg}
       \NT{int}~\mid~\tacconstr
\SEPDEF
\DEFNT{fix-spec}
       \KWD{(}~\NT{ident}~\STAR{\NT{binder}}~\OPT{\NT{annot}}
       ~\KWD{:}~\taclconstr~\KWD{)}
\SEPDEF
\DEFNT{intro-patterns}
       \STAR{\NT{intro-pattern}}
\SEPDEF
\DEFNT{intro-pattern}
       \NT{name}
\nlsep \TERM{[}~\NT{intro-patterns}~\STARGR{\TERMbar~\NT{intro-patterns}}
       ~\TERM{]}
\nlsep \KWD{(}~\NT{intro-pattern}~\STARGR{\KWD{,}~\NT{intro-pattern}}
       ~\KWD{)}
\SEPDEF
\DEFNT{with-names}
%       \KWD{as}~\TERM{[}~\STAR{\NT{ident}}~\STARGR{\TERMbar~\STAR{\NT{ident}}}
%       ~\TERM{]}
       \KWD{as}~\NT{intro-pattern}
\SEPDEF
\DEFNT{eliminator}
       \TERM{using}~\NT{constr-with-bindings}
\SEPDEF
\DEFNT{constr-with-bindings}
       % dangling ``with'' of ``fix'' can conflict with ``with''
       \tacconstr~\OPT{\NT{with-binding-list}}
\SEPDEF
\DEFNT{with-binding-list}
       \KWD{with}~\NT{binding-list}
\SEPDEF
\DEFNT{binding-list}
       \PLUS{\tacconstr}
\nlsep \PLUS{\NT{simple-binding}}
\SEPDEF
\DEFNT{simple-binding}
       \KWD{(}~\NT{quantified-hyp}~\KWD{:=}~\taclconstr~\KWD{)}
\SEPDEF
\DEFNT{red-flag}
       \TERM{beta} ~\mid~ \TERM{iota} ~\mid~ \TERM{zeta}
       ~\mid~ \TERM{delta} ~\mid~
       \TERM{delta}~\OPT{\TERM{-}}~\TERM{[}~\PLUS{\NT{reference}}~\TERM{]}
\SEPDEF
\DEFNT{clause}
       \KWD{in}~\TERM{*}
\nlsep \KWD{in}~\TERM{*}~\KWD{$\vdash$}~\OPT{\NT{concl-occ}}
\nlsep \KWD{in}~\OPT{\NT{hyp-ident-list}} ~\KWD{$\vdash$} ~\OPT{\NT{concl-occ}}
\nlsep \KWD{in}~\OPT{\NT{hyp-ident-list}}
\SEPDEF
\DEFNT{hyp-ident-list}
       \NT{hyp-ident}
\nlsep \NT{hyp-ident}~\KWD{,}~\NT{hyp-ident-list}
\SEPDEF
\DEFNT{hyp-ident}
       \NT{ident}
\nlsep \KWD{(}~\TERM{type}~\TERM{of}~\NT{ident}~\KWD{)}
\nlsep \KWD{(}~\TERM{value}~\TERM{of}~\NT{ident}~\KWD{)}
\SEPDEF
\DEFNT{concl-occ}
       \TERM{*} ~\NT{occurrences}
\SEPDEF
\DEFNT{pattern-occ}
       \tacconstr ~\NT{occurrences}
\SEPDEF
\DEFNT{unfold-occ}
       \NT{reference}~\NT{occurrences}
\SEPDEF
\DEFNT{occurrences}
       ~\OPTGR{\KWD{at}~\PLUS{\NT{int}}}
\SEPDEF
\DEFNT{hint-bases}
       \KWD{with}~\TERM{*}
\nlsep \KWD{with}~\PLUS{\NT{ident}}
\SEPDEF
\DEFNT{auto-args}
       \OPT{\NT{num}}~\OPTGR{\TERM{adding}~\TERM{[}~\PLUS{\NT{reference}}
       ~\TERM{]}}~\OPT{\TERM{destructuring}}~\OPTGR{\TERM{using}~\TERM{tdb}}
\end{rules}

\subsection{Ltac}

%% Currently, there are conflicts with keyword \KWD{in}: in the following,
%% has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
%% \begin{center}
%% \texttt{let x := simpl in ...}
%% \end{center}


\begin{rules}
\DEFNT{tactic}
       \NT{tactic} ~\KWD{;} ~\NT{tactic}  &5 &\RNAME{Then}
\nlsep \NT{tactic} ~\KWD{;}~\TERM{[} ~\OPT{\NT{tactic-seq}} ~\TERM{]}
         &5 &\RNAME{Then-seq}
%%
\nlsep \TERM{try} ~\NT{tactic}     &3R &\RNAME{Try}
\nlsep \TERM{do} ~\NT{int-or-var} ~\NT{tactic}
\nlsep \TERM{repeat} ~\NT{tactic}
\nlsep \TERM{progress} ~\NT{tactic}
\nlsep \TERM{info} ~\NT{tactic}
\nlsep \TERM{abstract}~\NTL{tactic}{2}~\OPTGR{\TERM{using}~\NT{ident}}
%%
\nlsep \NT{tactic} ~\TERMbarbar ~\NT{tactic} &2R &\RNAME{Orelse}
%%
\nlsep \KWD{fun} ~\PLUS{\NT{name}} ~\KWD{$\Rightarrow$}
       ~\NT{tactic}  &1 &\RNAME{Fun-tac}
\nlsep \KWD{let} ~\NT{let-clauses} ~\KWD{in} ~\NT{tactic}
\nlsep \KWD{let} ~\TERM{rec} ~\NT{rec-clauses} ~\KWD{in} ~\NT{tactic}
\nlsep \KWD{match}~\OPT{\TERM{reverse}}~\TERM{goal}~\KWD{with}
       ~\OPT{\TERMbar}~\OPT{\NT{match-goal-rules}} ~\KWD{end}
\nlsep \KWD{match} ~\NT{tactic} ~\KWD{with}
       ~\OPT{\TERMbar}~\OPT{\NT{match-rules}} ~\KWD{end}
\nlsep \TERM{first}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
\nlsep \TERM{solve}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
\nlsep \TERM{idtac}
\nlsep \TERM{fail} ~\OPT{\NT{num}} ~\OPT{\NT{string}}
\nlsep \TERM{constr}~\KWD{:}~\tacconstr
\nlsep \TERM{ipattern}~\KWD{:}~\NT{intro-pattern}
\nlsep \NT{term-ltac}
\nlsep \NT{reference}~\STAR{\NT{tactic-arg}}  &&\RNAME{call-tactic}
\nlsep \NT{simple-tactic}
%%
\nlsep \NT{tactic-atom}  &0 &\RNAME{atomic}
\nlsep \KWD{(} ~\NT{tactic} ~\KWD{)}
\SEPDEF
\DEFNT{tactic-arg}
       \TERM{ltac}~\KWD{:}~\NTL{tactic}{0}
\nlsep \TERM{ipattern}~\KWD{:}~\NT{intro-pattern}
\nlsep \NT{term-ltac}
\nlsep \NT{tactic-atom}
\nlsep \tacconstr
\SEPDEF
\DEFNT{term-ltac}
       \TERM{fresh} ~\OPT{\NT{string}}
\nlsep \TERM{context} ~\NT{ident} ~\TERM{[} ~\taclconstr ~\TERM{]}
\nlsep \TERM{eval} ~\NT{red-expr} ~\KWD{in} ~\tacconstr
\nlsep \TERM{type} ~\tacconstr
\SEPDEF
\DEFNT{tactic-atom}
       \NT{reference}
\nlsep \TERM{()}
\SEPDEF
\DEFNT{tactic-seq}
       \NT{tactic} ~\TERMbar ~\NT{tactic-seq}
\nlsep \NT{tactic}
\end{rules}



\begin{rules}
\DEFNT{let-clauses}
       \NT{let-clause} ~\STARGR{\KWD{with}~\NT{let-clause}}
\SEPDEF
\DEFNT{let-clause}
       \NT{ident} ~\STAR{\NT{name}} ~\KWD{:=} ~\NT{tactic}
\SEPDEF
\DEFNT{rec-clauses}
       \NT{rec-clause} ~\KWD{with} ~\NT{rec-clauses}
\nlsep \NT{rec-clause}
\SEPDEF
\DEFNT{rec-clause}
       \NT{ident} ~\PLUS{\NT{name}} ~\KWD{:=} ~\NT{tactic}
\SEPDEF
\DEFNT{match-goal-rules}
       \NT{match-goal-rule}
\nlsep \NT{match-goal-rule} ~\TERMbar ~\NT{match-goal-rules}
\SEPDEF
\DEFNT{match-goal-rule}
       \NT{match-hyps-list} ~\TERM{$\vdash$} ~\NT{match-pattern}
       ~\KWD{$\Rightarrow$} ~\NT{tactic}
\nlsep \KWD{[}~\NT{match-hyps-list} ~\TERM{$\vdash$} ~\NT{match-pattern}
       ~\KWD{]}~\KWD{$\Rightarrow$} ~\NT{tactic}
\nlsep \KWD{_} ~\KWD{$\Rightarrow$} ~\NT{tactic}
\SEPDEF
\DEFNT{match-hyps-list}
       \NT{match-hyps} ~\KWD{,} ~\NT{match-hyps-list}
\nlsep \NT{match-hyps}
\SEPDEF
\DEFNT{match-hyps}
       \NT{name} ~\KWD{:} ~\NT{match-pattern}
\SEPDEF
\DEFNT{match-rules}
       \NT{match-rule}
\nlsep \NT{match-rule} ~\TERMbar ~\NT{match-rules}
\SEPDEF
\DEFNT{match-rule}
       \NT{match-pattern} ~\KWD{$\Rightarrow$} ~\NT{tactic}
\nlsep \KWD{_} ~\KWD{$\Rightarrow$} ~\NT{tactic}
\SEPDEF
\DEFNT{match-pattern}
       \TERM{context}~\OPT{\NT{ident}}
       ~\TERM{[} ~\NT{constr-pattern} ~\TERM{]}  &&\RNAME{subterm}
\nlsep \NT{constr-pattern}
\SEPDEF
\DEFNT{constr-pattern}
       \tacconstr
\end{rules}

\subsection{Other tactics}

\begin{rules}
\EXTNT{simple-tactic}
       \TERM{rewrite} ~\NT{orient} ~\NT{constr-with-bindings}
         ~\OPTGR{\KWD{in}~\NT{ident}}
\nlsep \TERM{replace} ~\tacconstr ~\KWD{with} ~\tacconstr
         ~\OPTGR{\KWD{in}~\NT{ident}}
\nlsep \TERM{replace} ~\OPT{\NT{orient}} ~\tacconstr
         ~\OPTGR{\KWD{in}~\NT{ident}}
\nlsep \TERM{symplify_eq} ~\OPT{\NT{quantified-hyp}}
\nlsep \TERM{discriminate} ~\OPT{\NT{quantified-hyp}}
\nlsep \TERM{injection} ~\OPT{\NT{quantified-hyp}}
\nlsep \TERM{conditional}~\NT{tactic}~\TERM{rewrite}~\NT{orient}
         ~\NT{constr-with-bindings}~\OPTGR{\KWD{in}~\NT{ident}}
\nlsep \TERM{dependent}~\TERM{rewrite}~\NT{orient}~\NT{ident}
\nlsep \TERM{cutrewrite}~\NT{orient}~\tacconstr
         ~\OPTGR{\KWD{in}~\NT{ident}}
\nlsep \TERM{absurd} ~\tacconstr
\nlsep \TERM{contradiction}
\nlsep \TERM{autorewrite}~\NT{hint-bases}~\OPTGR{\KWD{using}~\NT{tactic}}
\nlsep \TERM{refine}~\tacconstr
\nlsep \TERM{setoid_replace} ~\tacconstr ~\KWD{with} ~\tacconstr
\nlsep \TERM{setoid_rewrite} ~\NT{orient} ~\tacconstr
\nlsep \TERM{subst} ~\STAR{\NT{ident}}
%% eqdecide.ml4
\nlsep \TERM{decide}~\TERM{equality} ~\OPTGR{\tacconstr~\tacconstr}
\nlsep \TERM{compare}~\tacconstr~\tacconstr
%% eauto
\nlsep \TERM{eexact}~\tacconstr
\nlsep \TERM{eapply}~\NT{constr-with-bindings}
\nlsep \TERM{prolog}~\TERM{[}~\STAR{\tacconstr}~\TERM{]}
         ~\NT{quantified-hyp}
\nlsep \TERM{eauto}~\OPT{\NT{quantified-hyp}}~\OPT{\NT{quantified-hyp}}
         ~\NT{hint-bases}
\nlsep \TERM{eautod}~\OPT{\NT{quantified-hyp}}~\OPT{\NT{quantified-hyp}}
         ~\NT{hint-bases}
%% tauto
\nlsep \TERM{tauto}
\nlsep \TERM{simplif}
\nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}}
\nlsep \TERM{linearintuition}~\OPT{\NT{num}}
%% plugins/cc
\nlsep \TERM{cc}
%% plugins/field
\nlsep \TERM{field}~\STAR{\tacconstr}
%% plugins/firstorder
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
%%\nlsep \TERM{gtauto}
\nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
%% plugins/fourier
\nlsep \TERM{fourierZ}
%% plugins/funind
\nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr}
%% plugins/jprover
\nlsep \TERM{jp}~\OPT{\NT{num}}
%% plugins/omega
\nlsep \TERM{omega}
%% plugins/ring
\nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
\nlsep \TERM{ring}~\STAR{\tacconstr}
%% plugins/romega
\nlsep \TERM{romega}
\SEPDEF
\DEFNT{orient}
       \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$}
\end{rules}

\section{Grammar of commands}

New symbols:
$$ \TERM{.}
~~ \TERM{..}
~~ \TERM{\tt >->}
~~ \TERM{:$>$}
~~ \TERM{$<$:}
$$

New keyword:
$$ \KWD{where}
$$

\subsection{Classification of commands}

\begin{rules}
\DEFNT{vernac}
       \TERM{Time}~\NT{vernac}  &2~~ &\RNAME{Timing}
%%
\nlsep \NT{gallina}~\TERM{.}    &1
\nlsep \NT{command}~\TERM{.}
\nlsep \NT{syntax}~\TERM{.}
\nlsep \TERM{[}~\PLUS{\NT{vernac}}~\TERM{]}~\TERM{.}
%%
\nlsep \OPTGR{\NT{num}~\KWD{:}}~\NT{subgoal-command}~\TERM{.} ~~~&0
\SEPDEF
\DEFNT{subgoal-command}
       \NT{check-command}
\nlsep %\OPT{\TERM{By}}~
   \NT{tactic}~\OPT{\KWD{..}}
\end{rules}

\subsection{Gallina and extensions}

\begin{rules}
\DEFNT{gallina}
       \NT{thm-token}~\NT{ident}~\STAR{\NT{binder-let}}~\KWD{:}~\NT{constr}
\nlsep \NT{def-token}~\NT{ident}~\NT{def-body}
\nlsep \NT{assum-token}~\NT{assum-list}
\nlsep \NT{finite-token}~\NT{inductive-definition}
      ~\STARGR{\KWD{with}~\NT{inductive-definition}}
\nlsep \TERM{Fixpoint}~\NT{fix-decl}~\STARGR{\KWD{with}~\NT{fix-decl}}
\nlsep \TERM{CoFixpoint}~\NT{fix-decl}~\STARGR{\KWD{with}~\NT{fix-decl}}
\nlsep \TERM{Scheme}~\NT{scheme}~\STARGR{\KWD{with}~\NT{scheme}}
%% Extension: record
\nlsep \NT{record-tok}~\OPT{\TERM{$>$}}~\NT{ident}~\STAR{\NT{binder-let}}
       ~\KWD{:}~\NT{constr}~\KWD{:=}
       ~\OPT{\NT{ident}}~\KWD{\{}~\NT{field-list}~\KWD{\}}
\nlsep \TERM{Ltac}~\NT{ltac-def}~\STARGR{~\TERM{with}~\NT{ltac-def}}
\end{rules}

\begin{rules}
\DEFNT{thm-token}
   \TERM{Theorem} ~\mid~ \TERM{Lemma} ~\mid~ \TERM{Fact} ~\mid~ \TERM{Remark}
\SEPDEF
\DEFNT{def-token}
   \TERM{Definition} ~\mid~ \TERM{Let} ~\mid~
   \OPT{\TERM{Local}}~\TERM{SubClass}
\SEPDEF
\DEFNT{assum-token}
    \TERM{Hypothesis} ~\mid~ \TERM{Variable} ~\mid~ \TERM{Axiom} ~\mid~
    \TERM{Parameter}
\SEPDEF
\DEFNT{finite-token}
    \TERM{Inductive} ~\mid~ \TERM{CoInductive}
\SEPDEF
\DEFNT{record-tok}
    \TERM{Record} ~\mid~ \TERM{Structure}
\end{rules}


\begin{rules}
\DEFNT{def-body}
       \STAR{\NT{binder-let}}~\NT{type-cstr}~\KWD{:=}
       ~\OPT{\NT{reduce}}~\NT{constr}
\nlsep \STAR{\NT{binder-let}}~\KWD{:}~\NT{constr}
\SEPDEF
\DEFNT{reduce}
       \TERM{Eval}~\NT{red-expr}~\KWD{in}
\SEPDEF
\DEFNT{ltac-def}
       \NT{ident}~\STAR{\NT{name}}~\KWD{:=}~\NT{tactic}
\SEPDEF
\DEFNT{rec-definition}
       \NT{fix-decl}~\OPT{\NT{decl-notation}}
\SEPDEF
\DEFNT{inductive-definition}
       \OPT{\NT{string}}~\NT{ident}~\STAR{\NT{binder-let}}~\KWD{:}
       ~\NT{constr}~\KWD{:=}
       ~\OPT{\TERMbar}~\OPT{\NT{constructor-list}}
       ~\OPT{\NT{decl-notation}}
\SEPDEF
\DEFNT{constructor-list}
       \NT{constructor}~\TERMbar~\NT{constructor-list}
\nlsep \NT{constructor}
\SEPDEF
\DEFNT{constructor}
       \NT{ident}~\STAR{\NT{binder-let}}\OPTGR{\NT{coerce-kwd}~\NT{constr}}
\SEPDEF
\DEFNT{decl-notation}
       \TERM{where}~\NT{string}~\TERM{:=}~\NT{constr}
\SEPDEF
\DEFNT{field-list}
       \NT{field}~\KWD{;}~\NT{field-list}
\nlsep \NT{field}
\SEPDEF
\DEFNT{field}
       \NT{ident}~\OPTGR{\NT{coerce-kwd}~\NT{constr}}
\nlsep \NT{ident}~\NT{type-cstr-coe}~\KWD{:=}~\NT{constr}
\SEPDEF
\DEFNT{assum-list}
       \PLUS{\GR{\KWD{(}~\NT{simple-assum-coe}~\KWD{)}}}
\nlsep \NT{simple-assum-coe}
\SEPDEF
\DEFNT{simple-assum-coe}
       \PLUS{\NT{ident}}~\NT{coerce-kwd}~\NT{constr}
\SEPDEF
\DEFNT{coerce-kwd} \TERM{:$>$} ~\mid~ \KWD{:}
\SEPDEF
\DEFNT{type-cstr-coe} \OPTGR{\NT{coerce-kwd}~\NT{constr}}
\SEPDEF
\DEFNT{scheme}
       \NT{ident}~\KWD{:=}~\NT{dep-scheme}~\KWD{for}~\NT{reference}
       ~\TERM{Sort}~\NT{sort}
\SEPDEF
\DEFNT{dep-scheme}
       \TERM{Induction}~\mid~\TERM{Minimality}
\end{rules}

\subsection{Modules and sections}

\begin{rules}
\DEFNT{gallina}
       \TERM{Module}~\NT{ident}~\STAR{\NT{mbinder}}~\OPT{\NT{of-mod-type}}
       ~\OPTGR{\KWD{:=}~\NT{mod-expr}}
\nlsep \TERM{Module}~\KWD{Type}~\NT{ident}~\STAR{\NT{mbinder}}
       ~\OPTGR{\KWD{:=}~\NT{mod-type}}
\nlsep \TERM{Declare}~\TERM{Module}~\NT{ident}~\STAR{\NT{mbinder}}
       ~\OPT{\NT{of-mod-type}}
       ~\OPTGR{\KWD{:=}~\NT{mod-expr}}
\nlsep \TERM{Section}~\NT{ident}
\nlsep \TERM{Chapter}~\NT{ident}
\nlsep \TERM{End}~\NT{ident}
%%
\nlsep \TERM{Require}~\OPT{\NT{export-token}}~\OPT{\NT{specif-token}}
       ~\PLUS{\NT{reference}}
\nlsep \TERM{Require}~\OPT{\NT{export-token}}~\OPT{\NT{specif-token}}
       ~\NT{string}
\nlsep \TERM{Import}~\PLUS{\NT{reference}}
\nlsep \TERM{Export}~\PLUS{\NT{reference}}
\SEPDEF
\DEFNT{export-token}
       \TERM{Import} ~\mid~ \TERM{Export}
\SEPDEF
\DEFNT{specif-token}
       \TERM{Implementation} ~\mid~ \TERM{Specification}
\SEPDEF
\DEFNT{mod-expr}
       \NT{reference}
\nlsep \NT{mod-expr}~\NT{mod-expr} & L
\nlsep \KWD{(}~\NT{mod-expr}~\KWD{)}
\SEPDEF
\DEFNT{mod-type}
       \NT{reference}
\nlsep \NT{mod-type}~\KWD{with}~\NT{with-declaration}
\SEPDEF
\DEFNT{with-declaration}
                                                          %on forcera les ( )
                                                          %si exceptionnellemt
                                                          %un fixpoint ici
       \TERM{Definition}~\NT{ident}~\KWD{:=}~\NTL{constr}{} %{100}
\nlsep \TERM{Module}~\NT{ident}~\KWD{:=}~\NT{reference}
\SEPDEF
\DEFNT{of-mod-type}
       \KWD{:}~\NT{mod-type}
\nlsep \TERM{$<$:}~\NT{mod-type}
\SEPDEF
\DEFNT{mbinder}
       \KWD{(}~\PLUS{\NT{ident}}~\KWD{:}~\NT{mod-type}~\KWD{)}
\end{rules}

\begin{rules}
\DEFNT{gallina}
       \TERM{Transparent}~\PLUS{\NT{reference}}
\nlsep \TERM{Opaque}~\PLUS{\NT{reference}}
\nlsep \TERM{Canonical}~\TERM{Structure}~\NT{reference}~\OPT{\NT{def-body}}
\nlsep \TERM{Coercion}~\OPT{\TERM{Local}}~\NT{reference}~\NT{def-body}
\nlsep \TERM{Coercion}~\OPT{\TERM{Local}}~\NT{reference}~\KWD{:}
       ~\NT{class-rawexpr}~\TERM{$>->$}~\NT{class-rawexpr}
\nlsep \TERM{Identity}~\TERM{Coercion}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:}
       ~\NT{class-rawexpr}~\TERM{$>->$}~\NT{class-rawexpr}
\nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}~\TERM{[}~\STAR{\NT{num}}~\TERM{]}
\nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}
\nlsep \TERM{Implicit}~\KWD{Type}~\PLUS{\NT{ident}}~\KWD{:}~\NT{constr}
\SEPDEF
\DEFNT{command}
       \TERM{Comments}~\STAR{\NT{comment}}
\nlsep \TERM{Pwd}
\nlsep \TERM{Cd}~\OPT{\NT{string}}
\nlsep \TERM{Drop} ~\mid~ \TERM{ProtectedLoop} ~\mid~\TERM{Quit}
%%
\nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{ident}
\nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{string}
\nlsep \TERM{Declare}~\TERM{ML}~\TERM{Module}~\PLUS{\NT{string}}
\nlsep \TERM{Locate}~\NT{locatable}
\nlsep \TERM{Add}~\OPT{\TERM{Rec}}~\TERM{LoadPath}~\NT{string}~\OPT{\NT{as-dirpath}}
\nlsep \TERM{Remove}~\TERM{LoadPath}~\NT{string}
\nlsep \TERM{Add}~\OPT{\TERM{Rec}}~\TERM{ML}~\TERM{Path}~\NT{string}
%%
\nlsep \KWD{Type}~\NT{constr}
\nlsep \TERM{Print}~\NT{printable}
\nlsep \TERM{Print}~\NT{reference}
\nlsep \TERM{Inspect}~\NT{num}
\nlsep \TERM{About}~\NT{reference}
%%
\nlsep \TERM{Search}~\NT{reference}~\OPT{\NT{in-out-modules}}
\nlsep \TERM{SearchPattern}~\NT{constr-pattern}~\OPT{\NT{in-out-modules}}
\nlsep \TERM{SearchRewrite}~\NT{constr-pattern}~\OPT{\NT{in-out-modules}}
\nlsep \TERM{SearchAbout}~\NT{reference}~\OPT{\NT{in-out-modules}}
\nlsep \TERM{SearchAbout}~\TERM{[}~\STAR{\NT{ref-or-string}}~\TERM{]}\OPT{\NT{in-out-modules}}
\nlsep \KWD{Set}~\NT{ident}~\OPT{\NT{opt-value}}
\nlsep \TERM{Unset}~\NT{ident}
\nlsep \KWD{Set}~\NT{ident}~\NT{ident}~\OPT{\NT{opt-value}}
\nlsep \KWD{Set}~\NT{ident}~\NT{ident}~\PLUS{\NT{opt-ref-value}}
\nlsep \TERM{Unset}~\NT{ident}~\NT{ident}~\STAR{\NT{opt-ref-value}}
%%
\nlsep \TERM{Print}~\TERM{Table}~\NT{ident}~\NT{ident}
\nlsep \TERM{Print}~\TERM{Table}~\NT{ident}
\nlsep \TERM{Add}~\NT{ident}~\OPT{\NT{ident}}~\PLUS{\NT{opt-ref-value}}
%%
\nlsep \TERM{Test}~\NT{ident}~\OPT{\NT{ident}}~\STAR{\NT{opt-ref-value}}
%%
\nlsep \TERM{Remove}~\NT{ident}~\OPT{\NT{ident}}~\PLUS{\NT{opt-ref-value}}
\SEPDEF
\DEFNT{check-command}
       \TERM{Eval}~\NT{red-expr}~\KWD{in}~\NT{constr}
\nlsep \TERM{Check}~\NT{constr}
\SEPDEF
\DEFNT{ref-or-string}
       \NT{reference}
\nlsep \NT{string}
\end{rules}

\begin{rules}
\DEFNT{printable}
       \TERM{Term}~\NT{reference}
\nlsep \TERM{All}
\nlsep \TERM{Section}~\NT{reference}
\nlsep \TERM{Grammar}~\NT{ident}
\nlsep \TERM{LoadPath}
\nlsep \TERM{Module}~\OPT{\KWD{Type}}~\NT{reference}
\nlsep \TERM{Modules}
\nlsep \TERM{ML}~\TERM{Path}
\nlsep \TERM{ML}~\TERM{Modules}
\nlsep \TERM{Graph}
\nlsep \TERM{Classes}
\nlsep \TERM{Coercions}
\nlsep \TERM{Coercion}~\TERM{Paths}~\NT{class-rawexpr}~\NT{class-rawexpr}
\nlsep \TERM{Tables}
% \nlsep \TERM{Proof}~\NT{reference}  % Obsolete, useful in V6.3 ??
\nlsep \TERM{Hint}~\OPT{\NT{reference}}
\nlsep \TERM{Hint}~\TERM{*}
\nlsep \TERM{HintDb}~\NT{ident}
\nlsep \TERM{Scopes}
\nlsep \TERM{Scope}~\NT{ident}
\nlsep \TERM{Visibility}~\OPT{\NT{ident}}
\nlsep \TERM{Implicit}~\NT{reference}
\SEPDEF
\DEFNT{class-rawexpr}
       \TERM{Funclass}~\mid~\TERM{Sortclass}~\mid~\NT{reference}
\SEPDEF
\DEFNT{locatable}
       \NT{reference}
\nlsep \TERM{File}~\NT{string}
\nlsep \TERM{Library}~\NT{reference}
\nlsep \NT{string}
\SEPDEF
\DEFNT{opt-value}
       \NT{ident} ~\mid~ \NT{string}
\SEPDEF
\DEFNT{opt-ref-value}
       \NT{reference} ~\mid~ \NT{string}
\SEPDEF
\DEFNT{as-dirpath}
       \KWD{as}~\NT{reference}
\SEPDEF
\DEFNT{in-out-modules}
       \TERM{inside}~\PLUS{\NT{reference}}
\nlsep \TERM{outside}~\PLUS{\NT{reference}}
\SEPDEF
\DEFNT{comment}
       \NT{constr}
\nlsep \NT{string}
\end{rules}

\subsection{Other commands}

%% TODO: min/maj pas a jour
\begin{rules}
\EXTNT{command}
       \TERM{Debug}~\TERM{On}
\nlsep \TERM{Debug}~\TERM{Off}
%% TODO: vernac
\nlsep \TERM{Add}~\TERM{setoid}~\tacconstr~\tacconstr~\tacconstr
\nlsep \TERM{Add}~\TERM{morphism}~\tacconstr~\KWD{:}~\NT{ident}
\nlsep \TERM{Derive}~\TERM{inversion_clear}
         ~\OPT{\NT{num}}~\NT{ident}~\NT{ident}
\nlsep \TERM{Derive}~\TERM{inversion_clear}
         ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
\nlsep \TERM{Derive}~\TERM{inversion}
         ~\OPT{\NT{num}}~\NT{ident}~\NT{ident}
\nlsep \TERM{Derive}~\TERM{inversion}
         ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
\nlsep \TERM{Derive}~\TERM{dependent}~\TERM{inversion_clear}
         ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
\nlsep \TERM{Derive}~\TERM{dependent}~\TERM{inversion}
         ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
%% Correctness: obsolete ?
%\nlsep Correctness
%\nlsep Global Variable
%% TODO: extraction
\nlsep Extraction ...
%% field
\nlsep \TERM{Add}~\TERM{Field}~\tacconstr~\tacconstr~\tacconstr
         ~\tacconstr~\tacconstr~\tacconstr
\nlcont~~~~\tacconstr~\tacconstr~\OPT{\NT{minus-div}}
%% funind
\nlsep \TERM{Functional}~\TERM{Scheme}~\NT{ident}~\KWD{:=}
         ~\TERM{Induction}~\KWD{for}~\tacconstr
         ~\OPTGR{\KWD{with}~\PLUS{\tacconstr}}
%% ring
\nlsep \TERM{Add}~\TERM{Ring}~\tacconstr~\tacconstr~\tacconstr
         ~\tacconstr~\tacconstr~\tacconstr
\nlcont~~~~\tacconstr~\tacconstr~\KWD{[}~\PLUS{\tacconstr}~\KWD{]}
\nlsep \TERM{Add}~\TERM{Semi}~\TERM{Ring}~\tacconstr~\tacconstr~\tacconstr
         ~\tacconstr~\tacconstr~\tacconstr
\nlcont~~~~\tacconstr~\KWD{[}~\PLUS{\tacconstr}~\KWD{]}
\nlsep \TERM{Add}~\TERM{Abstract}~\TERM{Ring}~\tacconstr~\tacconstr~\tacconstr
         ~\tacconstr~\tacconstr~\tacconstr
\nlcont~~~~\tacconstr~\tacconstr
\nlsep \TERM{Add}~\TERM{Abstract}~\TERM{Semi}~\TERM{Ring}~\tacconstr
         ~\tacconstr~\tacconstr~\tacconstr~\tacconstr~\tacconstr
\nlcont~~~~\tacconstr
\nlsep \TERM{Add}~\TERM{Setoid}~\TERM{Ring}~\tacconstr~\tacconstr~\tacconstr
         ~\tacconstr~\tacconstr~\tacconstr
\nlcont~~~~\tacconstr~\tacconstr~\tacconstr~\tacconstr~\tacconstr~\tacconstr
         ~\tacconstr~\KWD{[}~\PLUS{\tacconstr}~\KWD{]}
\nlsep \TERM{Add}~\TERM{Setoid}~\TERM{Semi}~\TERM{Ring}~\tacconstr~\tacconstr
         ~\tacconstr~\tacconstr~\tacconstr~\tacconstr
\nlcont~~~~\tacconstr~\tacconstr~\tacconstr~\tacconstr~\tacconstr
         ~\KWD{[}~\PLUS{tacconstr}~\KWD{]}
\SEPDEF
\DEFNT{minus-div}
       \KWD{with}~\NT{minus-arg}~\NT{div-arg}
\nlsep \KWD{with}~\NT{div-arg}~\NT{minus-arg}
\SEPDEF
\DEFNT{minus-arg}
       \TERM{minus}~\KWD{:=}~\tacconstr
\SEPDEF
\DEFNT{div-arg}
       \TERM{div}~\KWD{:=}~\tacconstr
\end{rules}

\begin{rules}
\EXTNT{command}
       \TERM{Write}~\TERM{State}~\NT{ident}
\nlsep \TERM{Write}~\TERM{State}~\NT{string}
\nlsep \TERM{Restore}~\TERM{State}~\NT{ident}
\nlsep \TERM{Restore}~\TERM{State}~\NT{string}
\nlsep \TERM{Reset}~\NT{ident}
\nlsep \TERM{Reset}~\TERM{Initial}
\nlsep \TERM{Back}~\OPT{\NT{num}}
\end{rules}

\subsection{Proof-editing commands}

\begin{rules}
\EXTNT{command}
       \TERM{Goal}~\NT{constr}
\nlsep \TERM{Proof}~\OPT{\NT{constr}}
\nlsep \TERM{Proof}~\KWD{with}~\NT{tactic}
\nlsep \TERM{Abort}~\OPT{\TERM{All}}
\nlsep \TERM{Abort}~\NT{ident}
\nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
\nlsep \TERM{Qed}
\nlsep \TERM{Save}~\NT{ident}
\nlsep \TERM{Defined}~\OPT{\NT{ident}}
\nlsep \TERM{Suspend}
\nlsep \TERM{Resume}~\OPT{\NT{ident}}
\nlsep \TERM{Restart}
\nlsep \TERM{Undo}~\OPT{\NT{num}}
\nlsep \TERM{Focus}~\OPT{\NT{num}}
\nlsep \TERM{Unfocus}
\nlsep \TERM{Show}~\OPT{\NT{num}}
\nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}}
\nlsep \TERM{Show}~\TERM{Node}
\nlsep \TERM{Show}~\TERM{Script}
\nlsep \TERM{Show}~\TERM{Existentials}
\nlsep \TERM{Show}~\TERM{Tree}
\nlsep \TERM{Show}~\TERM{Conjecture}
\nlsep \TERM{Show}~\TERM{Proof}
\nlsep \TERM{Show}~\TERM{Intro}
\nlsep \TERM{Show}~\TERM{Intros}
%% Correctness: obsolete ?
%%\nlsep \TERM{Show}~\TERM{Programs}
\nlsep \TERM{Hint}~\OPT{\TERM{Local}}~\NT{hint}~\OPT{\NT{inbases}}
%% PrintConstr not documented
\end{rules}


\begin{rules}
\DEFNT{constr-body}
       \NT{type-cstr}~\KWD{:=}~\NT{constr}
\SEPDEF
\DEFNT{hint}
       \TERM{Resolve}~\PLUS{\NTL{constr}{9}}
\nlsep \TERM{Immediate}~\PLUS{\NTL{constr}{9}}
\nlsep \TERM{Unfold}~\PLUS{\NT{reference}}
\nlsep \TERM{Constructors}~\PLUS{\NT{reference}}
\nlsep \TERM{Extern}~\NT{num}~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
\nlsep \TERM{Destruct}~\NT{ident}~\KWD{:=}~\NT{num}~\NT{destruct-loc}
       ~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
\nlsep \TERM{Rewrite}~\NT{orient}~\PLUS{\NTL{constr}{9}}
       ~\OPTGR{\KWD{using}~\NT{tactic}}
\SEPDEF
\DEFNT{inbases}
       \KWD{:}~\PLUS{\NT{ident}}
\SEPDEF
\DEFNT{destruct-loc}
       \TERM{Conclusion}
\nlsep \OPT{\TERM{Discardable}}~\TERM{Hypothesis}
\end{rules}


\subsection{Syntax extensions}

\begin{rules}
\DEFNT{syntax}
       \TERM{Open}~\TERM{Scope}~\NT{ident}
\nlsep \TERM{Close}~\TERM{Scope}~\NT{ident}
\nlsep \TERM{Delimit}~\TERM{Scope}~\NT{ident}~\KWD{with}~\NT{ident}
\nlsep \TERM{Bind}~\TERM{Scope}~\NT{ident}~\KWD{with}~\PLUS{\NT{class-rawexpr}}
\nlsep \TERM{Arguments}~\TERM{Scope}~\NT{reference}
       ~\TERM{[}~\PLUS{\NT{name}}~\TERM{]}
\nlsep \TERM{Infix}~\OPT{\TERM{Local}} %%% ~\NT{prec}~\OPT{\NT{num}}
       ~\NT{string}~\KWD{:=}~\NT{reference}~\OPT{\NT{modifiers}}
       ~\OPT{\NT{in-scope}}
\nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{string}~\KWD{:=}~\NT{constr}
       ~\OPT{\NT{modifiers}}~\OPT{\NT{in-scope}}
\nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:=}~\NT{constr}
       ~\OPT{\KWD{(}\TERM{only~\TERM{parsing}\KWD{)}}}
\nlsep \TERM{Reserved}~\TERM{Notation}~\OPT{\TERM{Local}}~\NT{string}
       ~\OPT{\NT{modifiers}}
\nlsep \TERM{Tactic}~\TERM{Notation}~\NT{string}~\STAR{\NT{tac-production}}
       ~\KWD{:=}~\NT{tactic}
\SEPDEF
\DEFNT{modifiers}
       \KWD{(}~\NT{mod-list}~\KWD{)}
\SEPDEF
\DEFNT{mod-list}
       \NT{modifier}
\nlsep \NT{modifier}~\KWD{,}~\NT{mod-list}
\SEPDEF
\DEFNT{modifier}
       \NT{ident}~\KWD{at}~\NT{num}
\nlsep \NT{ident}~\STARGR{\KWD{,}~\NT{ident}}~\KWD{at}~\NT{num}
\nlsep \KWD{at}~\TERM{next}~\TERM{level}
\nlsep \KWD{at}~\TERM{level}~\NT{num}
\nlsep \TERM{left}~\TERM{associativity}
\nlsep \TERM{right}~\TERM{associativity}
\nlsep \TERM{no}~\TERM{associativity}
\nlsep \NT{ident}~\NT{syntax-entry}
\nlsep \TERM{only}~\TERM{parsing}
\nlsep \TERM{format}~\NT{string}
\SEPDEF
\DEFNT{in-scope}
       \KWD{:}~\NT{ident}
\SEPDEF
\DEFNT{syntax-entry}
       \TERM{ident}~\mid~\TERM{global}~\mid~\TERM{bigint}
\SEPDEF
\DEFNT{tac-production}
       \NT{string}
\nlsep \NT{ident}~\TERM{(}~\NT{ident}~\TERM{)}
%%% \SEPDEF
%%% \DEFNT{prec}
%%%       \TERM{LeftA}~\mid~\TERM{RightA}~\mid~\TERM{NonA}
\end{rules}

\end{document}