The Coq mailing list

[Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>]

Hello.

On 18.08.2015 21:09, Guillaume Melquiond wrote:
> On 18/08/2015 17:10, Christoph-Simon Senjak wrote:
>
> > > > I am trying to use Native-Coq to compile some of my code, and it ...
> > > > sometimes ... works, and sometimes it doesn't, with no apparent reason.
>
> > I cloned from https://github.com/maximedenes/native-coq.git, commit
> > 7f6f7379b76c9c6240ab8083960a6531efa301c8 (which is the current one).
>
> Unless you have a reason to use such an outdated fork, I suggest using
> Coq itself. The 8.5 branch (and all the 8.5 betas) contains this
> native_compute mechanism.

The main reason for using native-coq is that it has the "PArray" 
library, which appears to implement diffarrays. Coq 8.5beta2 does not 
have this library. I could build bindings for diffarrays myself, but I 
preferred them because they were "built in". I really need Arrays, 
IntMaps are too slow. DiffArrays seem to be fast enough in my tests.

Is something similar in the newer Coq versions? Because I could not find it.

Regards,
Christoph