The Coq mailing list

[Holden Lee <holdenlee AT alum.mit.edu>]

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

..

More complicated: how can I print in backtracking proofs?

  tactic1 := (...); if succeed then print "Tactic 1 succeeds" else print "Tactic 1 fails."

 

  (tactic1 || tactic2)

Thanks,

Holden

(Sorry about accidentally sending the email before.)

On Tue, May 5, 2015 at 6:23 PM, Holden Lee <holdenlee AT alum.mit.edu> wrote: