The Coq mailing list

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

Thank you. I see that it's better to ask Ubuntu people why they keep 
such an old version in their repository:)
Or just compile it myself at the end. Anyway, if someone knows what 
exactly happened between two versions that causes
such behavior, I'm curious to know.

Karen

On 4/22/14, 8:51 PM, Adam Chlipala wrote:
> 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?