coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Anomaly" with crush

From: Tom Prince <tom.prince AT ualberta.net>
To: Chris Casinghino <chris.casinghino AT gmail.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "Anomaly" with crush
Date: Fri, 18 Feb 2011 01:12:33 -0500

On 2011-02-17, Chris Casinghino wrote:
> OK, I have reduced this to a very small example with no cpdt
> dependency. Looks like it's clearly a coq bug. Perhaps someone
> running the latest svn version can check whether or not it still
> exists?

Yes. http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2483

[Coq-Club] "Anomaly" with crush, Chris Casinghino
- Re: [Coq-Club] "Anomaly" with crush, Adam Chlipala
  - Re: [Coq-Club] "Anomaly" with crush, Chris Casinghino
    - Re: [Coq-Club] "Anomaly" with crush, Tom Prince
      - [Coq-Club] Monads in Coq, AUGER Cedric
        
        Re: [Coq-Club] Monads in Coq, ahrens
        
        Re: [Coq-Club] Monads in Coq, alexandre p
        
        Re: [Coq-Club] Monads in Coq, Adam Chlipala
        
        Re: [Coq-Club] Monads in Coq, Thomas Strathmann