coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Adam Chlipala <adam AT chlipala.net>
To: Chris Casinghino <chris.casinghino AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "Anomaly" with crush
Date: Tue, 15 Feb 2011 16:06:05 -0500

Chris Casinghino wrote:

The following simple code snippet causes coq to complain "Anomaly:
unknown meta ?122. Please report." along with a larger error,
reproduced below. This sounds like a coq error, but the example uses
the cpdt crush tactic.

I'm going to take the error message at face value and assume that this is a bug that needs fixing in Coq. :-)

[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