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 /plugins/extraction/miniml.mli | |
| 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 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 0bf1ff952b..5a19cc3f59 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -71,8 +71,7 @@ type ml_ind_packet = { ip_logical : bool; ip_sign : signature; ip_vars : identifier list; - ip_types : (ml_type list) array; - mutable ip_optim_id_ok : bool option + ip_types : (ml_type list) array } (* [ip_nparams] contains the number of parameters. *) |