The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I am using Hugo's patch:

I put the patch on "http://pauillac.inria.fr/~herbelin/doc". Since it
is short and indifferently applicable to 8.2, 8.3, trunk, I did not
created a github branch for it.

Vladimir.

PS I'll comment on the rest of the stuff later. 

On May 18, 2011, at 7:46 AM, Tom Prince wrote:

On 2011-05-18, Bruno Barras wrote:

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.

I am not sure what Vladimir is using, but I post a patch a allow
disabling universe checking a few weeks ago to coqdev. The patch is also
available here:

https://github.com/tomprince/coq/tree/inconsistent

 Tom