Extraction: better dependency computation (after optimisations)

When doing monolithic extraction, the initial dependency graph
may turn to be too broad thanks to later optimisations. We now do
an extra dependency pass at the end, killing more useless code.

In addition, when doing an "Extract Constant t => ...", if t
isn't an axiom, we don't include the dependencies of the body of t.

This may break earlier extraction setups (with or without Extract
Constant), since they may take advantage of objects that were earlier
"wrongly" included in the extracted code. The fix is simple : just
add these missing objects to the extraction command-line.
 


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11239 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions