Prooftree draws proof trees during interactive proof development with Proof General. One can inspect goals and proof commands and check where existential variables were introduced and instantiated. Currently, Prooftree does only work for Coq.