\section*{The Coq kernel}

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

The modules of the kernel are organized as follows.

TODO