The Coq mailing list

[David Baelde <david.baelde AT gmail.com>]

Hi list,

The issue has been sorted out thanks to Christine Paulin & Guillaume 
Melquiond.

On Sat, Dec 17, 2011 at 12:25 PM, David Baelde 
<david.baelde AT gmail.com>
 wrote:
> (** *** Definition of cpos *)
> Class cpo  `{o:ord D} : Type := mk_cpo
>  {D0 : D; lub: forall (f:nat -m> D), D;
> ...
>  Eval compute in (let (_,_,_) := cpoU in True).

The problem is that nat -m> D (monotonic functions from nat to D)
relies on the instance of (ord nat) which itself is built using omega.
In my eval compute, the normal form requires normalizing the proof
built by omega, which is what takes forever. We'll make this more
opaque, and/or factor things differently.

Cheers,
-- 
David