The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

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.

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.

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