On 05/02/2015 09:56, Alain Frisch wrote:
> One possible work-around is to use an alternative implementation of the
> demarshaler (there is such a pure OCaml implementation in Frama-C).
> Another is to avoid the generic marshaling, either by writing a manual
> version for your specific data type or by generating it from your type
> definitions (à la bin-prot, I assume).

Both workarounds would not work. Indeed, we use closure marshalling in
Coq, which is not supported by the two proposed implementations.

(Plus, that would be so slow I do not even want to think about it.)

PMP