The Coq mailing list

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

Hello.

On 21.09.2016 12:54, Maxime Dénès wrote:
> Hello,
>
> I'm sorry, it is indeed confusing.
>
> The original "native-coq" repository is the one you found on github. It
> contains a modified version of Coq with native code compilation and
> primitive integers and arrays.
>
> That version of Coq is loosely based on Coq 8.4, so it is indeed quite
> outdated. Note that the native code compilation part has been integrated
> in Coq, so native-coq is relevant only if you need primitive integers or
> arrays.

Indeed, I am interested in the diffarray-implementation.

> Since other users have asked for it, I'll try to port these integers and
> arrays to a more recent version of Coq, and will keep you posted. It
> should take a week or so.

Thank You
CSS

> Maxime.
>
> On 09/21/16 12:37, Christoph-Simon Senjak wrote:
> > Hello.
> >
> > I found several repositories of native-coq, most of them seem to be
> > forks. What is the original repository of native-coq? I found [1]  which
> > is by Maxime Dénès who is an author of the paper [2] so this is probably
> > a good source, but it hasn't been updated since 2015 and it appears to
> > be forked from some svn-branch.
> >
> > Regards,
> > Christoph-Simon Senjak
> >
> > [1]:https://github.com/maximedenes/native-coq
> > [2]:https://coq.inria.fr/files/GTCoq2013_denes.pdf