There's a separate project that solves this problem (CertiCoq https://www.cs.princeton.edu/~appel/certicoq/ https://www.cs.princeton.edu/~appel/certicoq/). It's

There's a separate project that solves this problem (CertiCoq https://www.cs.princeton.edu/~appel/certicoq/ https://www.cs.princeton.edu/~appel/certicoq/). It's making progress, but these things take time. :)