The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Perhaps the important missing piece of information here is that 8.3 and 
8.4 are effectively different "major versions" of Coq, in terms of the 
extent of reorganization that is common when adding 0.1 or more to a Coq 
version number. It won't surprise me if you're just seeing the result of 
a big standard-library refactoring.  Coq 8.3 was first released in 2010, 
and it's rather out of date today, regardless of the patch level.

On 04/22/2014 08:44 AM, Karen Sargsyan wrote:
> 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?