The Coq mailing list

[Karen Sargsyan <karsar AT ibms.sinica.edu.tw>]

Hi all,

If I do the following sequence on Ubuntu with Coq 8.3pl4 (ocaml 3.12.1):

Coq < Require Export ZArith.
Coq < Definition any: Z:= Z.div 2 3.

then result is: "Error: The reference Z.div was not found in the current 
environment"

On Mac OS X with 8.4pl2 OCaml 4.00.1 it defines "any".

So apparently there is some incompatibility between 8.3pl4 and 8.4pl2 in 
case of ZArith (something knows).
Is it so, or it's a bug in Ubuntu Coq package?

Thanks,
Karen