aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/modutil.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-29 16:36:55 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-29 16:36:55 +0000
commit2d83621457a1ea7f1955c7ab994abbec9d025ba9 (patch)
treec2a8161d53ac07efbbf2d9e54cbf817cbe3f3272 /plugins/extraction/modutil.ml
parentbafaf20a401546562924773016fcf051ee7ba8ec (diff)
coqdep: honor dependencies of "Load"ed files
Imagine A.v "Load"s B.v and that B.v "Require"s C. Before this commit we get: A.vo: A.v B.v After this commit we get: A.vo: A.v B.v C.vo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/modutil.ml')
0 files changed, 0 insertions, 0 deletions