The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Gregory Malecha wrote:
> 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.

This seems to be the same problem as for debug printing within pure 
parts of Haskell programs.  The tactic terms of Ltac are like a monadic 
sublanguage.  Unfortunately, I don't have a simple solution to suggest.

> 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.

There _is_ a fairly general but painful way to "fix" the problem, which 
is to convert all term-returning functions to continuation-passing style:

Ltac foo x k :=
 idtac x;
 k 1.

Goal True.
 match goal with
   | [ |- ?G ] =>
     foo G ltac:(fun r => pose r)
 end.