The Coq mailing list

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

Hi coq-club and Adam,

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.

  Require Import List.
  Require Import Tactics.

  Theorem crush_error : forall (P : list nat -> Prop),
      (forall (A B : list nat), P (app A B)) -> False.
  Proof.
    crush.

This example is a little silly, but is of course reduced from a much
larger program.  I actually get this error quite a bit when trying to
use crush in my current development, so any help would be highly
appreciated.

I tried stepping through crush's behavior with the ltac debugging
mode, but I'm too much of a tactic newbie to make sense of the output.
I'm running coq 8.3 pl1, and have the latest version of the cpdt
tools.

Here is the longer error message.  Thanks!

  Toplevel input, characters 8-13:
  In nested Ltac calls to "crush", "crush'", "rewriter" (bound to
  autorewrite with cpdt in *;
   repeat
    (match goal with
     | H:?P
       |- _ =>
           match P with
           | context [JMeq.JMeq] => fail 1
           | _ =>
               (rewrite H; [ idtac ]) ||
                 (rewrite H; [ idtac | solve [ crush' lemmas invOne ] ]) ||
                   (rewrite H;
                     [ idtac
                     | solve
                     [ crush' lemmas invOne ]
                     | solve
                     [ crush' lemmas invOne ] ])
           end
     end; autorewrite with cpdt in *)) and "rewrite H", last call failed.
  Anomaly: unknown meta ?122. Please report.

--Chris Casinghino