Added new syntax definition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4100 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 1387 insertions, 0 deletions

diff --git a/doc/check-grammar b/doc/check-grammar
new file mode 100755
index 0000000000..67da1bc513
--- /dev/null
+++ b/doc/check-grammar
@@ -0,0 +1,50 @@
+#!/bin/bash
+# This scripts checks that the new grammar of Coq as defined in syntax-v8.tex
+# is consistent in the sense that all invoked non-terminals are defined
+
+defined-nt() {
+  grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\
+    sort | sort -u
+}
+
+used-nt() {
+  cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\
+    sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u
+}
+
+used-term() {
+  cat syntax-v8.tex | tr \\\\ \\n | grep "^TERM{.*}" |\
+    sed -e "s|^TERM{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1\|terminal | sort -u
+}
+
+used-kwd() {
+  cat syntax-v8.tex | tr \\\\ \\n | grep "^KWD{.*}" |\
+    sed -e "s|^KWD{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1 | sort -u
+}
+
+defined-nt > def
+used-nt > use
+used-term > use-t
+used-kwd > use-k
+diff def use > df
+
+###############################
+echo
+if grep ^\> df > /dev/null 2>&1 ; then
+  echo Undefined non-terminals:
+  echo ========================
+  echo
+  grep ^\> df | sed -e "s|^> ||"
+  echo
+fi
+if grep ^\< df > /dev/null 2>&1 ; then
+  echo Unused non-terminals:
+  echo =====================
+  echo
+  grep ^\< df | sed -e "s|^< ||"
+  echo
+fi
+#echo Used terminals:
+#echo ===============
+#echo
+#cat use-t
\ No newline at end of file
diff --git a/doc/memo-v8.tex b/doc/memo-v8.tex
new file mode 100644
index 0000000000..a25eef8478
--- /dev/null
+++ b/doc/memo-v8.tex
@@ -0,0 +1,274 @@
+
+\documentclass{article}
+
+\usepackage{verbatim}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{array}
+\usepackage{fullpage}
+
+\author{B.~Barras}
+\title{A introduction to syntax of Coq V8}
+
+%% Le _ est un caractère normal
+\catcode`\_=13
+\let\subscr=_
+\def_{\ifmmode\sb\else\subscr\fi}
+
+\def\NT#1{\langle\textit{#1}\rangle}
+\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
+\def\TERM#1{\textsf{\bf #1}}
+
+\newenvironment{transbox}
+  {\begin{center}\tt\begin{tabular}{l|ll} \hfil\textrm{V7} & \hfil\textrm{V8} \\ \hline}
+  {\end{tabular}\end{center}}
+\def\TRANS#1#2
+  {\begin{tabular}[t]{@{}l@{}}#1\end{tabular} & 
+   \begin{tabular}[t]{@{}l@{}}#2\end{tabular} \\}
+\def\TRANSCOM#1#2#3
+  {\begin{tabular}[t]{@{}l@{}}#1\end{tabular} & 
+   \begin{tabular}[t]{@{}l@{}}#2\end{tabular} & #3 \\}
+
+\begin{document}
+
+\maketitle
+
+The goal of this document is to introduce by example to the new syntax of
+Coq. It is strongly recommended to read first the definition of the new
+syntax, but this document should also be useful for the eager user who wants
+to start with the new syntax quickly.
+
+
+\section{Main changes in terms w.r.t. V7}
+
+\subsection{Identifiers}
+
+The lexical conventions changed: \TERM{_} is not a regular identifier
+anymore. It is used in terms as a placeholder for subterms to be inferred
+at type-checking, and in patterns as a non-binding variable.
+
+\subsection{Precedence of application}
+
+In the new syntax, parentheses are not really part of the syntax of
+application. The precedence of application (10) is tighter than all
+prefix and infix notations. It makes ot possible to remove the parentheses
+in many contexts.
+
+\begin{transbox}
+\TRANS{(A x)->(f x)=(g y)}{A x -> f x = g y}
+\TRANS{(f [x]x)}{f (fun x => x)}
+\end{transbox}
+
+
+\subsection{Arithmetics and scopes}
+
+The specialized notation for \TERM{Z} and \TERM{R} (introduced by symbols \TERM{`} and \TERM{``}) have disappeared. They have been replaced by the general notion of scope.
+
+\begin{center}
+\begin{tabular}{l|l|l}
+type & scope name & key \\
+\hline
+types & type_scope & \TERM{T} \\
+\TERM{bool} & bool_scope & \\
+\TERM{nat} & nat_scope & \TERM{N} \\
+\TERM{Z} & Z_scope & \TERM{Z} \\
+\TERM{R} & R_scope & \TERM{R} \\
+\TERM{positive} & positive_scope & \TERM{P}
+\end{tabular}
+\end{center}
+
+In order to use notations of arithmetics on \TERM{Z}, its scope must be opened with command \verb+Open Scope Z_scope.+ Another possibility is using the scope change notation (\TERM{\%}). The latter notation is to be used when notations of several scopes appear in the same expression.
+
+In examples below, scope changes are not needed if the appropriate scope
+has been opened.
+\begin{transbox}
+\TRANSCOM{`0+x=x+0`}{0+x=x+0}{\textrm{Z_scope}}
+\TRANSCOM{``0 + [if b then ``1`` else ``2``]``}{0 + if b then 1 else 2}{\textrm{R_scope}}
+\TRANSCOM{(0)}{0}{\textrm{nat_scope}}
+\end{transbox}
+
+Below is a table that tells which notation is available in which. The
+relative precedences and associativity of operators is the same as in
+usual mathematics. See the reference manual for more details. However,
+it is important to remember that unlike V7, the type operators for
+product and sum are left associative, in order not to clash with
+arithmetic operators.
+
+\begin{center}
+\begin{tabular}{l|l}
+scope & notations \\
+\hline
+nat_scope & $+ ~- ~* ~< ~\leq ~> ~\geq$ \\
+Z_scope & $+ ~- ~* ~/ ~\TERM{mod} ~< ~\leq ~> ~\geq ~?=$ \\
+R_scope & $+ ~- ~* ~/ ~< ~\leq ~> ~\geq ~{}^2$ \\
+type_scope & $* ~+$ \\
+bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{!!}$
+\end{tabular}
+\end{center}
+(Note: $\leq$ is written \TERM{$<=$}, and the square notation uses iso-latin
+character 178)
+
+
+
+\subsection{Notation for implicit arguments}
+
+The explicitation of arguments is closer to the \emph{bindings} notation in
+tactics.
+
+\begin{transbox}
+\TRANS{f 1!x 2!y}{f @1:=x @2:=y}
+\TRANS{!f x y}{@f x y}
+\end{transbox}
+
+
+\subsection{Universal quantification}
+
+The universal quantification and dependent product types are now
+materialized with the \TERM{forall} keyword before the binders and a
+comma after the binders.
+
+The syntax of binders also changed significantly. A binder can simply be
+a name when its type can be inferred. In other cases, the name and the type
+of the variable are put between parentheses. When several consecutive
+variables have the same type, they can be grouped. Finally, if all variables
+have the same type parentheses can be omitted.
+
+\begin{transbox}
+\TRANS{(x:A)B}{forall (x:~A), B ~~\textrm{or}~~ forall x:~A, B}
+\TRANS{(x,y:nat)P}{forall (x y :~nat), P ~~\textrm{or}~~ forall x y :~nat, P}
+\TRANS{(x,y:nat;z:A)P}{forall (x y :~nat) (z:A), P}
+\TRANS{(x,y,z,t:?)P}{forall x y z t, P}
+\TRANS{(x,y:nat;z:?)P}{forall (x y :~nat) z, P}
+\end{transbox}
+
+\subsection{Abstraction}
+
+The notation for $\lambda$-abstraction follows that of universal
+quantification. The binders are surrounded by keyword \TERM{fun}
+and $\Rightarrow$ (\verb+=>+ in ascii).
+
+\begin{transbox}
+\TRANS{[x,y:nat; z](f a b c)}{fun (x y:nat) z => f a b c}
+\end{transbox}
+
+
+\subsection{Pattern-matching}
+
+Beside the usage of the keyword pair \TERM{match}/\TERM{with} instead of
+\TERM{Cases}/\TERM{of}, the main change is the notation for the type of
+branches and return type. It is no longer written between \TERM{$<$ $>$} before
+the \TERM{Cases} keyword, but interleaved with the destructured object.
+
+The idea is that for each destructured object, one may specify a variable
+name to tell how the branches type depend on this destructured object (case
+of a dependent elimination), and also how they depend on the value of the
+arguments of the inductive type of the destructured object. The type of
+branches is then given after the keyword \TERM{return}, unless it can be
+inferred.
+
+Moreover, when the destructured object is a variable, one may use this
+variable in the return type.
+
+\begin{transbox}
+\TRANS{Cases n of\\~~ O => O \\| (S k) => (1) end}{match n with\\~~ 0 => 0 \\| (S k) => 1 end}
+\TRANS{Cases m n of \\~~0 0 => t \\| ... end}{match m, n with \\~~0, 0 => t \\| .. end}
+\TRANS{<[n:nat](P n)>Cases T of ... end}{match T as n return P n with ... end}
+\TRANS{<[n:nat][p:(even n)]\~{}(odd n)>Cases p of\\~~ ... \\end}{match p in even n return \~{} odd n with\\~~ ...\\end}
+\end{transbox}
+
+
+\subsection{Fixpoints and cofixpoints}
+
+An easier syntax for non-mutual fixpoints is provided, making it very close
+to the usual notation for non-recursive functions. The decreasing argument
+is now indicated by an annotation between curly braces, regardless of the
+binders grouping. The annotation can be omitted if the binders introduce only
+one variable. The type of the result can be omitted if inferable.
+
+\begin{transbox}
+\TRANS{Fix plus\{plus [n:nat] : nat -> nat :=\\~~ [m]...\}}{fix plus (n m:nat) \{struct n\}: nat := ...}
+\TRANS{Fix fact\{fact [n:nat]: nat :=\\
+~~Cases n of\\~~~~ O -> (1) \\~~| (S k) => (mult n (fact k)) end\}}{fix fact
+  (n:nat) :=\\
+~~match n with \\~~~~0 => 1 \\~~| (S k) => n * fact k end}
+\end{transbox}
+
+There is a syntactic sugar for non-mutual fixpoints associated to a local
+definition:
+
+\begin{transbox}
+\TRANS{let f := Fix f \{f [x:A] : T := M\} in\\(g (f y))}{let fix f (x:A) : T := M in\\g (f x)}
+\end{transbox}
+
+The same applies to cofixpoints, annotations are not allowed in that case.
+
+\subsection{Notation for type cast}
+
+\begin{transbox}
+\TRANS{O :: nat}{0 : nat}
+\end{transbox}
+
+\section{Main changes in tactics w.r.t. V7}
+
+The main change is that all tactic names are lowercase. This also holds for
+Ltac keywords.
+
+\subsection{Ltac}
+
+Definitions of macros are introduced by \TERM{Ltac} instead of \TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive Definition}.
+
+Rules of a match command are not between square brackets anymore.
+
+Context (understand a term with a placeholder) instantiation \TERM{inst}
+became \TERM{context}. Syntax is unified with subterm matching.
+
+\begin{transbox}
+\TRANS{match t with [C[x=y]] => inst C[y=x]}{match t with context C[x=y] => context C[y=x]}
+\end{transbox}
+
+\subsection{List of arguments}
+
+Since the precedence of application is now very tight, tactics that take
+a list of terms would require to put parenthesis around each argument
+very often. In the new syntax, terms are separated by commas. Tactics
+affected by this change are: \TERM{pattern}, \TERM{unfold}, \TERM{fold},
+\TERM{generalize} and the list of dependent bindings of \TERM{apply},
+\TERM{elim}, \TERM{case}, \TERM{specialize}, \TERM{left}, \TERM{right},
+\TERM{exists}, \TERM{split} and \TERM{constructor}.
+
+\begin{transbox}
+\TRANS{Generalize t (f x)}{generalize t, f x}
+\TRANS{Apply t with (f x) b (g y)}{apply t with f x, b, g y}
+\end{transbox}
+
+\subsection{Occurrences}
+
+Occurences of a term are now listed after the term itself.
+\begin{transbox}
+\TRANS{Pattern 1 2 (f x) 3 4 d}{pattern (f x) 1 2, d 3 4}
+\end{transbox}
+
+\section{Main changes in vernacular commands w.r.t. V7}
+
+
+\subsection{Binders}
+
+The binders of vernacular commands changed in the same way as those of
+fixpoints. This also holds for parameters of inductive definitions.
+
+
+\begin{transbox}
+\TRANS{Definition x [a:A] : T := M}{Definition x (a:A) : T := M}
+\TRANS{Inductive and [A,B:Prop]: Prop := \\~~conj : A->B->(and A B)}%
+      {Inductive and (A B:Prop): Prop := \\~~conj : A -> B -> and A B}
+\end{transbox}
+
+\subsection{Hints}
+
+The syntax of \emph{extern} hints changed: the pattern and the tactic
+to be applied are separated by a \TERM{$\Rightarrow$}.
+\begin{transbox}
+\TRANS{Extern 4 (toto ?) Apply lemma}{Extern 4 toto _ => Apply lemma}
+\end{transbox}
+
+\end{document}
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
new file mode 100644
index 0000000000..c9d424ee7c
--- /dev/null
+++ b/doc/syntax-v8.tex
@@ -0,0 +1,1063 @@
+
+\documentclass{article}
+
+\usepackage{verbatim}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{array}
+\usepackage{fullpage}
+
+\author{B.~Barras}
+\title{A new syntax for Coq}
+
+%% 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}
+
+
+%% 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 optionaly 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}
+     \NT{letter}\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{int}         \PLUS{\NT{digit}}
+\SEPDEF
+\DEFNT{digit}       \CHAR{0}-\CHAR{9}
+\SEPDEF
+\DEFNT{letter}      \CHAR{a}-\CHAR{z}\mid\CHAR{A}-\CHAR{Z}
+                    \mid\NT{unicode-letter}\mid\NT{iso-latin-letter}
+
+\SEPDEF
+\DEFNT{string}      \CHAR{"}~\STARGR{\CHAR{$\backslash$"}\mid\CHAR{$\backslash\backslash$}\mid\NT{unicode-char}\mid\NT{iso-latin-char}}~\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{\%}
+$$
+
+Note that \TERM{struct} is not a reserved identifier.
+
+\section{Syntax of terms}
+
+\subsection{Core syntax}
+
+
+\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{\NT{constr}}      &10L  &\RNAME{expl-apply}
+\nlsep \NT{constr} ~ \KWD{\%} ~ \NT{ident}            &1L   &\RNAME{scope-chg}
+\nlsep \NT{atomic-constr}                             &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}~\STAR{\NT{binder}}~\NT{type-cstr}
+       ~\KWD{:=}~\NT{constr}
+       ~\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-patt}}~\KWD{)}~\OPT{\NT{return-type}}
+       ~\KWD{:=}~\NT{constr}~\KWD{in}~\NTL{constr}{200}
+          &&\RNAME{let-case}
+\nlsep \KWD{if}~\NT{constr}~\OPT{\NT{return-type}}
+       ~\KWD{then}~\NTL{constr}{200}~\KWD{else}~\NTL{constr}{200}
+          &&\RNAME{if-case}
+\SEPDEF
+\DEFNT{appl-arg}
+       \KWD{@}~\NT{int}~\!\KWD{:=}~\NTL{constr}{9}  &&\RNAME{impl-arg}
+\nlsep \NTL{constr}{9}
+\SEPDEF
+\DEFNT{atomic-constr}
+       \NT{reference}     && \RNAME{variables}
+\nlsep \NT{sort}          && \RNAME{CIC-sort}
+\nlsep \NT{int}           && \RNAME{number}
+\nlsep \KWD{_}            && \RNAME{hole}
+\nlsep \NT{meta-ident}    && \RNAME{meta/evar}
+\nlsep \KWD{(}~\NT{tuple}~\KWD{)}
+\nlsep \NT{match-expr}
+\SEPDEF
+\DEFNT{tuple}
+       \NT{constr}
+\nlsep \NT{tuple}~\KWD{,}~\NT{constr}               &&\RNAME{pair}
+\end{rules}
+
+
+
+\begin{rules}
+\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-patt}
+       \NT{name}
+\nlsep \NT{name} ~\KWD{,} ~\NT{let-patt}
+\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}}~\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{case-items}~\OPT{\NT{case-type}}~\KWD{with}
+  ~\OPT{\TERMbar}~\OPT{\NT{branches}}~\KWD{end}        &&\RNAME{match}
+\SEPDEF
+\DEFNT{case-items}
+       \NT{case-item} ~\KWD{,} ~\NT{case-items}
+\nlsep \NT{case-item}
+\SEPDEF
+\DEFNT{case-item}
+       \NTL{constr}{100}~\OPTGR{\KWD{as}~\NT{name}}
+       ~\OPTGR{\KWD{in}~\NTL{constr}{100}}
+\SEPDEF
+\DEFNT{case-type}
+       \KWD{return}~\NTL{constr}{100}
+\SEPDEF
+\DEFNT{return-type}
+       \OPTGR{\KWD{as}~\NT{name}}~\NT{case-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{int}                            &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)}
+
+$$
+\begin{array}{l|c}
+\text{Symbol} & \text{precedence} \\
+\hline
+\rightarrow, \leftrightarrow  & 80R \\
+\wedge           & 70R\\
+\vee             & 60R \\
+\tilde           & 55R \\
+=,\neq,<,>,\leq,\geq   & 50N \\
++,-,\text{unary minus} & 40L \\
+*,/,\text{inverse}     & 30L \\
+{\text{_}}^2     & 20L
+\end{array}
+$$
+
+Existential quantifier follows the \KWD{forall} notation (with same
+precedence 200), producing an iterated application to constant \TERM{Ex}.
+
+\begin{rules}
+\EXTNT{binder-constr}
+       \NT{quantifier-kwd}~\NT{binder-list}~\KWD{,}~\NTL{constr}{200} \\
+\SEPDEF
+\DEFNT{quantifier-kwd}
+       \TERM{ex} && \RNAME{Ex}
+\nlsep \TERM{ex_S} && \RNAME{sig}
+\nlsep \TERM{ex_T} && \RNAME{exT}
+\end{rules}
+
+\TERM{Ex2} \TERM{ExT2},, \TERM{sigS}, \TERM{sigT}, \TERM{sigS2},
+\TERM{sumor} and \TERM{sumbool} have no particular syntax.
+
+
+\subsection{Notations for records}
+
+These notations are not yet implemented.
+
+\begin{rules}
+\EXTNT{constr}
+       \NT{constr}~\TERM{.(}~\NT{constr}~\KWD{)} &1L~~ & \RNAME{proj}
+\nlsep \KWD{\{}~\NT{rfield}~\STARGR{\KWD{;}~\NT{rfield}}~\KWD{\}} &0
+    &\RNAME{constructor}
+\SEPDEF
+\EXTNT{pattern}
+       \KWD{\{}~\NT{field-patt}~\STARGR{\KWD{;}~\NT{field-patt}}~\KWD{\}}
+\SEPDEF
+\DEFNT{rfield}
+       \GR{\NT{reference}~\mid~\KWD{_}}~\KWD{:=}~\NT{constr}
+\SEPDEF
+\DEFNT{field-patt}
+       \GR{\NT{reference}~\mid~\KWD{_}}~\KWD{:=}~\NT{pattern}
+\end{rules}
+
+Note that $\NT{reference}~\NT{field}$ may also denote a record projection.
+The conflict with module access can be resolved at globalization time,
+depending whether the $\NT{reference}$ is a module or not.
+
+
+\section{Grammar of tactics}
+
+\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{name}}~\OPTGR{\TERM{after}~\NT{ident}}
+%%
+\nlsep \TERM{assumption}
+\nlsep \TERM{exact}~\NT{constr}
+%%
+\nlsep \TERM{apply}~\NT{constr-with-bindings}
+\nlsep \TERM{elim}~\NT{constr-with-bindings}~\OPT{\NT{eliminator}}
+\nlsep \TERM{elimtype}~\NT{constr}
+\nlsep \TERM{case}~\NT{constr-with-bindings}
+\nlsep \TERM{casetype}~\NT{constr}
+\nlsep \KWD{fix}~\OPT{\NT{ident}}~\NT{int}
+\nlsep \KWD{fix}~\NT{ident}~\NT{int}~\PLUS{\NT{fixdecl}}
+\nlsep \KWD{cofix}~\OPT{\NT{ident}}
+\nlsep \KWD{cofix}~\NT{ident}~\PLUS{\NT{fixdecl}}
+%%
+\nlsep \TERM{cut}~\NT{constr}
+\nlsep \TERM{assert}~\NT{constr}
+\nlsep \TERM{assert}~\NT{constr}~\KWD{:=}~\NT{constr}
+\nlsep \TERM{pose}~\NT{constr}
+\nlsep \TERM{pose}~\NT{constr}~\KWD{:=}~\NT{constr}
+\nlsep \TERM{generalize}~\NT{constr}~\STARGR{\KWD{,}~\NT{constr}}
+\nlsep \TERM{generalize}~\TERM{dependent}~\NT{constr}
+\nlsep \TERM{lettac}~\NT{ident}~\KWD{:=}~\NT{constr}~\NT{clause-pattern}
+\nlsep \TERM{instantiate}~\NT{int}~\NT{constr}
+%%
+\nlsep \TERM{specialize}~\OPT{\NT{int}}~\NT{constr-with-bindings}
+\nlsep \TERM{lapply}~\NT{constr}
+%%
+\nlsep \TERM{oldinduction}~\NT{quantified-hyp}
+\nlsep \TERM{induction}~\NT{induction-arg}~\OPT{\NT{eliminator}}
+       ~\OPT{\NT{with-names}}
+\nlsep \TERM{double}~\TERM{induction}~\NT{quantified-hyp}~\NT{quantified-hyp}
+\nlsep \TERM{olddestruct}~\NT{quantified-hyp}
+\nlsep \TERM{destruct}~\NT{induction-arg}~\OPT{\NT{eliminator}}
+       ~\OPT{\NT{with-names}}
+\nlsep \TERM{decompose}~\TERM{record}~\NT{constr}
+\nlsep \TERM{decompose}~\TERM{sum}~\NT{constr}
+\nlsep \TERM{decompose}~\TERM{[}~\PLUS{\NT{ltac-ref}}~\TERM{]}
+       ~\NT{constr}
+%%
+\nlsep ...
+\end{rules}
+
+\begin{rules}
+\EXTNT{simple-tactic}
+       \TERM{trivial}~\OPT{\NT{hint-bases}}
+\nlsep \TERM{auto}~\OPT{\NT{int}}~\OPT{\NT{hint-bases}}
+%%
+\nlsep \TERM{autotdb}~\OPT{\NT{int}}
+\nlsep \TERM{cdhyp}~\NT{ident}
+\nlsep \TERM{dhyp}~\NT{ident}
+\nlsep \TERM{dconcl}
+\nlsep \TERM{superauto}~\NT{auto-args}
+\nlsep \TERM{auto}~\OPT{\NT{int}}~\TERM{decomp}~\OPT{\NT{int}}
+%%
+\nlsep \TERM{clear}~\PLUS{\NT{ltac-id}}
+\nlsep \TERM{clearbody}~\PLUS{\NT{ltac-id}}
+\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{int}~\OPT{\NT{with-binding-list}}
+\nlsep \TERM{constructor}~\OPT{\NT{tactic}}
+%%
+\nlsep \TERM{reflexivity}
+\nlsep \TERM{symmetry}
+\nlsep \TERM{transitivity}
+%%
+\nlsep \NT{red-expr}~\NT{clause}
+\nlsep \TERM{change}~\NT{conversion}~\NT{clause}
+\SEPDEF
+\DEFNT{red-expr}
+       \TERM{red} ~\mid~ \TERM{hnf} ~\mid~ \TERM{simpl} ~\mid~
+       \TERM{compute}
+\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}~\NT{constr}~\STARGR{\KWD{,}~\NT{constr}}
+\nlsep \TERM{pattern}~\NT{pattern-occ}~\STARGR{\KWD{,}~\NT{pattern-occ}}
+\SEPDEF
+\DEFNT{conversion}
+       \STAR{\NT{int}}~\NT{constr}~\KWD{with}~\NT{constr}
+\nlsep \NT{constr}
+\end{rules}
+
+Conflicts exists between integers and constrs.
+
+\begin{rules}
+\DEFNT{ltac-id}
+       \NT{ident} ~\mid~ \NT{meta-ident}
+\SEPDEF
+\DEFNT{ltac-ref}
+      \NT{reference} ~\mid~ \NT{meta-ident}
+\SEPDEF
+\DEFNT{quantified-hyp}
+       \NT{int}~\mid~\NT{ident}
+\SEPDEF
+\DEFNT{induction-arg}
+       \NT{int}~\mid~\NT{constr}
+\SEPDEF
+\DEFNT{fixdecl}
+       \KWD{with}~\NT{ident}~\STAR{\NT{binder}}~\OPT{\NT{annot}}
+       ~\KWD{:}~\NTL{constr}{100}
+\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{]}
+\SEPDEF
+\DEFNT{eliminator}
+       \TERM{using}~\NT{constr-with-bindings}
+\SEPDEF
+\DEFNT{constr-with-bindings}
+       \NTL{constr}{100}~\OPT{\NT{with-binding-list}}
+\SEPDEF
+\DEFNT{with-binding-list}
+       \KWD{with}~\NT{binding-list}
+\SEPDEF
+\DEFNT{binding-list}
+       \PLUS{\NTL{constr}{9}}
+\nlsep \PLUS{\NT{simple-binding}}
+\SEPDEF
+\DEFNT{simple-binding}
+       \KWD{(}~\NT{quantified-hyp}~\KWD{:=}~\NT{constr}~\KWD{)}
+\SEPDEF
+\DEFNT{pattern-occ}
+       \NTL{constr}{9}~\STAR{\NT{int}}
+\SEPDEF
+\DEFNT{unfold-occ}
+       \NT{ltac-ref}~\STAR{\NT{int}}
+\SEPDEF
+\DEFNT{red-flag}
+       \TERM{beta} ~\mid~ \TERM{iota} ~\mid~ \TERM{zeta}
+       ~\mid~ \TERM{delta} ~\mid~
+       \TERM{delta}~\OPT{\TERM{-}}~\TERM{[}~\PLUS{\NT{ltac-ref}}~\TERM{]}
+\SEPDEF
+\DEFNT{clause}
+       \OPTGR{\KWD{in}~\NT{hyp-ident}}
+\SEPDEF
+\DEFNT{hyp-ident}
+       \NT{ident}
+\nlsep \KWD{(}~\TERM{type}~\TERM{of}~\NT{ident}~\KWD{)}
+\SEPDEF
+\DEFNT{clause-pattern}
+       \KWD{in}~\NT{pattern-hyp-list}
+\SEPDEF
+\DEFNT{pattern-hyp-list}
+       \STAR{\NT{int}}~\TERM{goal}
+\nlsep \STAR{\NT{int}}~\NT{ident}~\OPT{\NT{pattern-hyp-list}}
+\SEPDEF
+\DEFNT{hint-bases}
+       \KWD{with}~\TERM{*}
+\nlsep \KWD{with}~\PLUS{\NT{ident}}
+\SEPDEF
+\DEFNT{auto-args}
+       \OPT{\NT{int}}~\OPTGR{\TERM{adding}~\TERM{[}~\PLUS{\NT{reference}}
+       ~\TERM{]}}~\OPT{\TERM{destructuring}}~\OPTGR{\TERM{using}~\TERM{tdb}}
+\end{rules}
+
+
+\subsection{Ltac}
+
+Additional symbols are:
+$$ \TERM{'}
+~~ \KWD{;}
+~~ \TERM{()}
+~~ \TERM{$\vdash$}
+$$
+Additional reserved keywords are:
+$$ \TERM{orelse}
+~~ \TERM{using}
+$$
+
+Currently, there are conflicts with keyword \KWD{in}: in the following,
+the keyword must 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}     &3 &\RNAME{Try}
+\nlsep \TERM{do} ~\NT{tactic}
+\nlsep \TERM{repeat} ~\NT{tactic}
+\nlsep \TERM{progress} ~\NT{tactic}
+\nlsep \TERM{info} ~\NT{tactic}
+%%
+\nlsep \NT{tactic} ~\TERM{orelse} ~\NT{tactic} &2R &\RNAME{Orelse}
+%%
+\nlsep \KWD{fun} ~\PLUS{\NT{name}} ~\KWD{$\Rightarrow$}
+       ~\NT{tactic}  &1 &\RNAME{Fun-tac}
+\nlsep \TERM{rec} ~\NT{rec-clauses} ~\KWD{in} ~\NT{tactic}
+\nlsep \KWD{let} ~\NT{let-clauses} ~\KWD{in} ~\NT{tactic}
+\nlsep \KWD{match}~\OPT{\TERM{reverse}}~\TERM{context}~\KWD{with}
+       ~\OPT{\TERMbar}~\OPT{\NT{match-ctxt-rules}} ~\KWD{end}
+\nlsep \KWD{match} ~\NTL{constr}{100} ~\KWD{with}
+       ~\OPT{\TERMbar}~\OPT{\NT{match-rules}} ~\KWD{end}
+\nlsep \TERM{abstract}~\NT{tactic}~\OPTGR{\TERM{using}~\NT{ident}}
+\nlsep \TERM{first}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
+\nlsep \TERM{solve}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
+\nlsep \TERM{idtac}
+\nlsep \TERM{fail} ~\OPT{\NT{int}} ~\OPT{\NT{string}}
+\nlsep \TERM{fresh} ~\OPT{\NT{string}}
+\nlsep \TERM{context} ~\NT{ident} ~\TERM{[} ~\NT{constr} ~\TERM{]}
+\nlsep \TERM{eval} ~\NT{red-expr} ~\KWD{in} ~\NT{constr}
+\nlsep \TERM{check} ~\NT{constr}
+\nlsep \TERM{'} ~\NT{constr}
+\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{\bf '} ~\NTL{tactic}{0}
+\nlsep \NT{tactic-atom}
+\nlsep \NTL{constr}{9}
+\SEPDEF
+\DEFNT{tactic-atom}
+       \NT{reference}
+\nlsep \NT{meta-ident}
+\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}} ~\NT{type-cstr} ~\KWD{:=} ~\NT{tactic}
+\nlsep \NT{ident} ~\KWD{:} ~\NT{constr} ~\OPTGR{\KWD{:=}~\TERM{proof}}
+\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{$\Rightarrow$} ~\NT{tactic}
+\SEPDEF
+\DEFNT{match-ctxt-rules}
+       \NT{match-ctxt-rule}
+\nlsep \NT{match-ctxt-rule} ~\TERMbar ~\NT{match-ctxt-rules}
+\SEPDEF
+\DEFNT{match-ctxt-rule}
+       \NT{match-hyps-list} ~\TERM{$\vdash$} ~\NT{match-pattern}
+       ~\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}
+\SEPDEF
+\DEFNT{match-pattern}
+       \TERM{context}~\OPT{\NT{ident}}
+       ~\TERM{[} ~\NT{constr-pattern} ~\TERM{]}  &&\RNAME{subterm}
+\nlsep \NT{constr-pattern}
+\SEPDEF
+\DEFNT{constr-pattern}
+       \NT{constr}
+\end{rules}
+
+\section{Grammar of commands}
+
+New symbols:
+$$ \TERM{.}
+~~ \TERM{!!}
+~~ \TERM{\tt >->}
+~~ \TERM{:$>$}
+~~ \TERM{$<$:}
+$$
+
+\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{int}~\KWD{:}}~\NT{subgoal-command}~\TERM{.} ~~~&0
+\SEPDEF
+\DEFNT{subgoal-command}
+       \NT{check-command}
+\nlsep \OPT{\TERM{By}}~\OPT{\TERM{!!}}~\NT{tactic}
+\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{rec-definitions}
+\nlsep \TERM{CoFixpoint}~\NT{rec-definitions}
+\nlsep \TERM{Scheme}~\NT{scheme}~\STARGR{\KWD{with}~\NT{scheme}}
+%% Extension: record
+\nlsep \NT{record-tok}~\OPT{\TERM{$>$}}~\NT{ident}~\STAR{\NT{binder}}
+       ~\KWD{:}~\NT{constr}~\KWD{:=}
+       ~\OPT{\NT{ident}}~\KWD{\{}~\NT{assum-list}~\KWD{\}}
+\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{Local} ~\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}}~\NT{type-cstr}~\KWD{:=}
+       ~\OPT{\NT{reduce}}~\NT{constr}
+\nlsep \STAR{\NT{binder}}~\KWD{:}~\NT{constr}
+\SEPDEF
+\DEFNT{reduce}
+       \TERM{Eval}~\NT{red-expr}~\KWD{in}
+\SEPDEF
+\DEFNT{inductive-definition}
+       \OPT{\NT{string}}~\NT{ident}~\STAR{\NT{binder}}~\KWD{:}
+       ~\NT{constr}~\KWD{:=}
+       ~\OPT{\TERMbar}~\OPT{\NT{constructor-list}}
+\SEPDEF
+\DEFNT{constructor-list}
+       \NT{sbinder-coe}~\TERMbar~\NT{constructor-list}
+\nlsep \NT{sbinder-coe}
+\SEPDEF
+\DEFNT{sbinder-coe}
+       \PLUS{\NT{ident}}~\OPTGR{\NT{coerce-kwd}~\NT{constr}}
+\SEPDEF
+\DEFNT{assum-list}
+       \NT{sbinder-let-coe}~\KWD{;}~\NT{assum-list}
+\nlsep \NT{sbinder-let-coe}
+\SEPDEF
+\DEFNT{sbinder-let-coe}
+       \NT{sbinder-coe}
+\nlsep \NT{ident}~\NT{type-cstr}~\KWD{:=}~\NT{constr}
+\SEPDEF
+\DEFNT{coerce-kwd} \TERM{:$>$} ~\mid~ \KWD{:}
+\SEPDEF
+\DEFNT{rec-definitions}
+       \NT{rec-definition}~\STARGR{\KWD{with}~\NT{rec-definition}}
+\SEPDEF
+\DEFNT{rec-definition}
+       \NT{ident}~\STAR{\NT{binder}}~\OPT{\NT{annot}}~\NT{type-cstr}
+       ~\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} ~\mid~ \TERM{Closed}
+\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}
+       \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{Implicits}~\NT{reference}~\TERM{[}~\STAR{\NT{int}}~\TERM{]}
+\nlsep \TERM{Implicits}~\NT{reference}
+\nlsep \TERM{Implicit}~\TERM{Variable}~\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{Dump}~\TERM{Universes}~\OPT{\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}~\OPT{\NT{printable}}
+\nlsep \TERM{Print}~\NT{reference}
+\nlsep \TERM{Inspect}~\NT{int}
+%%
+\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}}
+\SEPDEF
+\DEFNT{check-command}
+       \TERM{Eval}~\NT{red-expr}~\KWD{in}~\NT{constr}
+\nlsep \TERM{Check}~\NT{constr}
+\end{rules}
+
+\begin{rules}
+\DEFNT{printable}
+       \TERM{Term}~\NT{reference}
+\nlsep \TERM{All}
+\nlsep \TERM{Section}~\NT{reference}
+\nlsep \TERM{Grammar}~\NT{ident}~\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}
+\nlsep \TERM{Hint}~\OPT{\NT{reference}}
+\nlsep \TERM{Hint}~\TERM{*}
+\nlsep \TERM{HintDb}~\NT{ident}
+\nlsep \TERM{Scope}~\NT{ident}
+\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}
+\nlsep \NT{int}
+\end{rules}
+
+\subsection{Switches}
+\begin{rules}
+\DEFNT{command}
+       \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}}
+\end{rules}
+
+\subsection{Other commands}
+
+
+\begin{rules}
+\DEFNT{command}
+       \TERM{Ltac}~\NT{ident}~\STAR{\NT{name}}~\KWD{:=}~\NT{tactic}
+\nlsep \TERM{Debug}~\TERM{On}
+\nlsep \TERM{Debug}~\TERM{Off}
+\end{rules}
+
+
+\begin{rules}
+\DEFNT{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{int}}
+\end{rules}
+
+\subsection{Proof-editing commands}
+
+\begin{rules}
+\DEFNT{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{int}~\NT{constr-body}
+\nlsep \TERM{Qed}
+\nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\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{int}}
+\nlsep \TERM{Focus}~\OPT{\NT{int}}
+\nlsep \TERM{Unfocus}
+\nlsep \TERM{Show}~\OPT{\NT{int}}
+\nlsep \TERM{Show}~\TERM{Implicits}~\OPT{\NT{int}}
+\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}
+\nlsep \TERM{Explain}~\TERM{Proof}~\OPT{\TERM{Tree}}~\STAR{\NT{int}}
+%% Go not documented
+\nlsep \TERM{Hint}~\TERM{Destruct}~\NT{destruct-loc}~\NT{int}
+       ~\NT{ident}~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
+\nlsep \TERM{Hint}~\NT{hint}~\OPT{\NT{hintbases}}
+%% PrintConstr not documented
+\end{rules}
+
+
+\begin{rules}
+\DEFNT{constr-body}
+       \NT{type-cstr}~\KWD{:=}~\NT{constr}
+\SEPDEF
+\DEFNT{hint}
+       \TERM{Resolve}~\NT{constr}~\STARGR{\KWD{,}~\NT{constr}}
+\nlsep \TERM{Immediate}~\NT{constr}~\STARGR{\KWD{,}~\NT{constr}}
+\nlsep \TERM{Unfold}~\PLUS{\NT{reference}}
+\nlsep \TERM{Constructors}~\PLUS{\NT{reference}}
+\nlsep \TERM{Extern}~\NT{int}~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
+\nlsep \TERM{Rewrite}~\NT{orient}~\NT{constr}~\STARGR{\TERM{,}~\NT{constr}}
+       ~\OPTGR{\KWD{using}~\NT{tactic}}
+\SEPDEF
+\DEFNT{hintbases}
+       \KWD{:}~\PLUS{\NT{ident}}
+\SEPDEF
+\DEFNT{orient}
+       \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$}
+\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{Delimits}~\TERM{Scope}~\NT{ident}~\KWD{with}~\NT{ident}
+\nlsep \TERM{Arguments}~\TERM{Scope}~\NT{reference}
+       ~\TERM{[}~\PLUS{\NT{name}}~\TERM{]}
+\nlsep \TERM{Infix}~\OPT{\TERM{Local}}~\NT{prec}~\OPT{\NT{int}}
+       ~\NT{string}~\NT{reference}~\OPT{\NT{modifiers}}
+       ~\OPT{\NT{in-scope}}
+\nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:=}~\NT{constr}
+       ~\OPT{\NT{modifiers}}~\OPT{\NT{in-scope}}
+\nlsep \TERM{Uninterpreted}~\TERM{Notation}~\OPT{\TERM{Local}}~\NT{string}
+       ~\OPT{\NT{modifiers}}
+\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}~\TERM{at}~\NT{int}
+\nlsep \NT{ident}~\STARGR{\KWD{,}~\NT{ident}}~\TERM{at}~\NT{int}
+\nlsep \TERM{at}~\TERM{level}~\NT{int}
+\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}
+\SEPDEF
+\DEFNT{in-scope}
+       \KWD{:}~\NT{ident}
+\SEPDEF
+\DEFNT{syntax-entry}
+       \TERM{ident}~\mid~\TERM{reference}~\mid~\NT{ident}
+\SEPDEF
+\DEFNT{prec}
+       \TERM{LeftA}~\mid~\TERM{RightA}~\mid~\TERM{NonA}
+\end{rules}
+
+\end{document}