I'm not aware of any work on this, but looking at the proof term it shouldn't be too difficult to compute these. Just do a dead variable/code elimination in the proof term and you should have your answer. Matching that back up to the tactic script might take some work though.
Post by Abhishek Anand Has someone worked on a tool which when given a finished proof, can try to prune (`clear`) as many hypotheses as early as possible during the proof? -- -- Abhishek http://www.cs.cornell.edu/~aa755/
You can simulate this by using the section mechanism: open a section, declare all hypothesis as "Hypothesis" or parameters, prove your lemma foo and close the section. Only used hypothesis will be quantified in foo.