How to trace all goals explicitly?

Stream: general

[Joseph Corneli]

tactic.target >>= tactic.trace tells me the current main goal, but I would like to see all of the goals.

tactic.get_goals >>= tactic.trace has meta-variables in it. Is there a printer option that fills them in? I've forgotten.

[Mario Carneiro]

mmap infer_type get_goals >>= trace