This repository contains a tool to compile Coq code written in an imperative style using a monad into the corresponding C code. It starts from the Coq code extracted as JSON by the internal extraction facility.
The source code is covered by CeCILL-A licence, see LICENSE.
The CoqC Development Team is:
- Veis Oudjail [email protected]
- Samuel Hym [email protected]