[Coq-Club] automated hypothesis pruning

[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?

[Gregory Malecha]

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/

[Pierre Courtieu]

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.

Hope this helps.

P