The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello,

Is there a way to determine if an Ltac variable binds a meta variable, i.e. a ?nn variable? In 8.2 and prior I had this Ltac definition:

Ltac meta X := 

  match X with

    | _ _ => fail 1

    | _ _ _ => fail 1

    | _ _ _ _ => fail 1

    | _ _ _ _ _ => fail 1

    | _ _ _ _ _ _ => fail 1

    | _ _ _ _ _ _ _ => fail 1

    | _ _ _ _ _ _ _ _ => fail 1

    | _ * _ => fail 1

    | X => fail 1

    | _ => idtac

  end.

Interestingly enough, terms with meta variables did not match themselves so all of the guards would fail until the end and the result would be a success. This behavior doesn't seem to work in 8.3 (possibly rightfully so), but is there another tactic that I can run?

Any pointers greatly appreciated. Thanks.

--
gregory malecha