\section*{Grammaire du langage}

\begin{figure}[ht]
  \termgrammar
  \caption{Termes}
  \label{fig:gram-terms}
\end{figure}

\begin{figure}[ht]
  \typegrammar
  \caption{Types}
  \label{fig:gram-types}
\end{figure}

On peut mettre des termes dans les types seulement lors de l'application
d'un type (bonne modélisation du positionement interne des termes ? ). 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "subset-typing"
%%% LaTeX-command: "TEXINPUTS=\"style:$TEXINPUTS\" latex"
%%% End: