The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[idtac] is already a kind of "whatever->string"

Goal Ture.

let x := constr:(1 + 1) in idtac x.

(* (1 + 1) *)

On Tue, Jun 18, 2013 at 12:33 AM, Math Prover <mathprover AT gmail.com> wrote:

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!