diff options
| author | letouzey | 2011-11-30 16:38:11 +0000 |
|---|---|---|
| committer | letouzey | 2011-11-30 16:38:11 +0000 |
| commit | 2f56532885d91b20b4c7b084abc4e49b82ab1c28 (patch) | |
| tree | 338dd5076436c9a9ef04130848f7f7c8a45499e4 /ide | |
| parent | 40f2181f1513cc72ce085688c88e703fbaaf1226 (diff) | |
Extraction: try to avoid issues with an Include directly inside a .v
This concerns only "monolithic" extraction (and not Extraction Library).
Typical situation is Vector.v containing an Include VectorDef.
Cf. the test-case of bug #2570.
Also kills two lines of dead code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14755 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions