GitLab

Use the local debian mirror instead of the global one
Only install the required packages, not all the recommended ones
Use a short expiring date for artifacts, in cases of quick succession of
CI builds, only the most recent is to be kept

Primitive operations in C world, such as `==`, `&&`, etc. are naturally
represented as non-monadic functions in Gallina.

With this patch, given this code:

    do x <- returnM (eqb y z) ;
    ...

the type for x is properly generated as the return type of eqb, without
requiring an explicit definition of a monadic lifting of eqb.

Since "." in Coq names are converted to "_" in C names, automatically
insert "_" between explicitly provided namespace and name for
dependencies

Of course, axioms cannot be converted but they can now appear in modules
and be correctly parsed

Update the name of University
Mention the example

This is required in Coq 8.9

Prepare for an evolution of that function

Show how to define a monad to provide support, how to write code in that
monad, how to use Coq extraction and how to call digger to convert the
code

version 0.2

Refactor the code parsing the JSON extracted from Coq.

Rewrite completely the conversion to C, splitting it in two stages:
- from the Coq AST to an intermediate representation corresponding to
  the part of Gallina that we can map to C,
- from that intermediate representation to C.

Use the standard Language.C library to produce the resulting C code, to
strengthen its quality.