The Coq mailing list

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

Hello,

I'm wondering if there is a good way to debug tactics that produce terms rather than manipulate goals. Normally I debug tactics with idtac, but it doesn't seem to work with these types of tactics. For example:

Ltac foo x := 

  constr:(1).

Ltac foo_debug x := 

  idtac "hello" ;

  constr:(1).

Goal True.

  match goal with

    | [ |- ?G ] => 

      let k := foo G in

      pose k

  end.

If I call foo then there isn't any problem, but if I call foo_debug, then things don't work. If I change "pose" to "idtac" then foo will cause 1 to be printed and foo_debug will cause "<tactic>" to be printed. Is there something that I could replace idtac with that will print something but not have this behavior?

Thank you.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/