The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 05/18/2011 11:44 AM, Robin Green wrote:
> It's also standard practice to include a file to automate the compilation
> (typically a Makefile), as Dan Grayson has done in his fork. That way
> people can reproduce the full compilation conveniently, without having to
> download all the old revisions of the compiled files.
>
> If you want, I can take care of all of this for you - including generating
> archives with generated files if you want - and you can just pull my
> changes into your repository.
>
>    

Hi,
As far as I understood, Vladimir is using a modified version of Coq 
(with universe constraints checking disabled in some way), so he would 
have to publish a patch to be applied on Coq sources.

Cheers,

Bruno.

--
Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14