The Coq mailing list

[Chris Casinghino <chris.casinghino AT gmail.com>]

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?

This code causes coq-8.3pl1 to respond "Anomaly: unknown meta
?2. Please report."  The code attempts to rewrite by something which
is not an equality, but coq should fail more gracefully (in a more
standard Ltac way).

  Require Import List.

  Theorem error : forall (P : list nat -> Prop),
      (forall (A B : list nat), P (app A B)) -> False.
  Proof.
    intros P H. rewrite H.

In the short term, is there a simple Ltac check I can add to my larger
tactic that will fail more gracefully if a hypothesis can not be used
as an argument to rewrite?

Thanks!

--Chris Casinghino




On Tue, Feb 15, 2011 at 4:06 PM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> 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. :-)
>