Version 8.1 of the Coq proof assistant is now the new stable version (http://coq.inria.fr/) Reproducible: Always
Thanks for the note and I've just bumped coq to 8.1pl1. ml@g.o folks! Unfortunately, coq-8.1pl1 badly fails to compile with ocaml-3.10.0; the patch posted on the coq website for ocaml-3.10.0 doesn't seem to work, but since I don't know ocaml at all it is hard to tell for me at the moment what the problem is. I'll try to have a look at it sometime but due to me not knowing ocaml at all this one may be difficult to fix. Thanks, Markus
(In reply to comment #1) > Unfortunately, coq-8.1pl1 badly fails to compile with ocaml-3.10.0; > the patch posted on the coq website for ocaml-3.10.0 doesn't seem > to work, but since I don't know ocaml at all it is hard to tell > for me at the moment what the problem is. I'll try to have a look at > it sometime but due to me not knowing ocaml at all this one may > be difficult to fix. imho don't waste your time doing this, it's definitely not a trivial thing to fix and afaik upstream has been working on it. The patch posted is supposed to be used with dev-ml/camlp5 but I've heard it still has issues with it. I'd say just wait for a new release, ocaml 3.10 still has other issues that block its unmasking, so one more or one less... And thanks for bumping coq !
Thanks much for your comments! I will wait then and please don't hesitate to ping me if anything needs to be done in the meantime.
