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 veis.oudjail@etudiant.univ-lille1.fr
- Samuel Hym samuel.hym@univ-lille1.fr