*** Very experimental and not branched ***

*** Very experimental and not branched ***

Exportation to OCaml partially implement in cic_exportation.

It can already export several files from the freescale development (also not
committed yet).

Still to be implemented:

 a) erasure of term dependencies from types
 b) extraction of "open" statements
    [ I do not know how to implement this! ]
 c) extraction from CurrentProof
 d) extraction from Let-In
 e) extraction from CoFix
 f) extraction from mutually recursive inductive types and Fix

Known bugs/missing features:

 1) All the "classical" ones (described, for instance, in Letouzey's papers).
    In particular, terms may diverge, singleton elimination and false
    elimination not implemented in the correct way, Obj.magic not generated
    where needed, etc.

 2) Name clashes can be generated by the extraction. OCaml keywords may be
    chosen. And so on.