Arnaud Spiwack wrote:
> This bug seems to have nothing to do with camlp4/5. I've seen this bug
> twice before, with two different version of OCaml (3.09.3 and 3.09.2
> namely), but always Coq 8.1pl2. It's rare, and I have no clue why they
> occur.

I don't insist, I just want a Coq which doesn't think that semirings
satisfy the cancelation law for addition (since I care about
distributive lattices, which are semirings without a cancelation law).

> One solution is to move to the trunk version of Coq (whose Makefile has
> been reengineered, and is far less surprising).

Will try an older version of Coq first. Thanks for the advice. I just
wanted to hear from someone that Coq was "Ocaml 3.10 ready".

Andrej