DIsplay proof term corresponding to tactics

Stream: new members

[Ricardo Prado Cunha]

Is there a way to view the proof term corresponding to some definition that uses tactics, similar to the Print command in Coq? I've tried looking for this but all I could find is the ? argument to some tactics like simp, while I'd want something that expands out an entire definition rather than a single tactic.

[Mario Carneiro]

#print

[Mario Carneiro]

or show_term to show the expression generated by a subterm or tactic

[Ricardo Prado Cunha]

#print is exactly what I was looking for; thanks!