The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi,

  With apologies for another newb question:

  In ltac, is there something like "whatever -> string" ?

  For example, I feel like my ltac skills would dramatically increase if I could do something like the following:

  Ltac blahblah :=

    match goal with

    | .. ?X .. =>

       idtac (whatever->string X);

    end.

  The point being that if I could somehow see what ltac patterns are being bound/matched to, it'd dramatically help me debug my ltac code.

  Right now: I'm using VimCoq/CoqIde, ... but I also have ProofGeneral/Emacs installed and working. I also know what with "idtac", I can print a string -- but I really want it to print a string representation of the clause/prop/varaible I'm matching against.

Thanks!