The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/05/2015 06:25 PM, Holden Lee wrote:
> How can I print in Coq? For example, What's the correct way to write this
> so that the tactic prints what it's doing?
>
> Ltac some_tactic:=
>    match goal with
> | [H : ?x = ?y |- _] => print ("rewriting "++(show H)); rewrite H
> ..

The tactics idtac and fail both can be used to print info during 
proofs.  The example above becomes:

Ltac some_tactic :=
   match goal with
   | H : ?x = ?y |- _ => idtac "rewriting" H; rewrite H
 ...

> More complicated: how can I print in backtracking proofs?
>
>    tactic1 := (...); if succeed then print "Tactic 1 succeeds" else print
> "Tactic 1 fails."
>
>    (tactic1 || tactic2)

Ltac tactic1 := tryif (...) then idtac "Tactic 1 succeeds" else fail 0 
"Tactic 1 fails".

-- Jonathan