path: root/kernel/doc.tex

\section*{The Coq kernel}

\ocwsection \label{kernel}
This section describes the \Coq\ kernel, which is a type checker for the \CCI.

The modules of the kernel are organized as follows.

TODO