diff options
author | 2011-11-30 16:38:11 +0000 | |
---|---|---|
committer | 2011-11-30 16:38:11 +0000 | |
commit | 2f56532885d91b20b4c7b084abc4e49b82ab1c28 (patch) | |
tree | 338dd5076436c9a9ef04130848f7f7c8a45499e4 | |
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
-rw-r--r-- | plugins/extraction/extraction.ml | 16 | ||||
-rw-r--r-- | plugins/extraction/miniml.mli | 3 |
2 files changed, 11 insertions, 8 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 549830fe7..2ab5bf9bf 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -351,10 +351,15 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if not (mib_equal mib mib0) then raise Not_found; ml_ind with Not_found -> - (* First, if this inductive is aliased via a Module, *) - (* we process the original inductive. *) - let equiv = - if kn_ord (canonical_mind kn) (user_mind kn) = 0 then + (* First, if this inductive is aliased via a Module, + we process the original inductive if possible. + When at toplevel of the monolithic case, we cannot do much + (cf Vector and bug #2570) *) + let equiv = + if lang () <> Ocaml || + (not (modular ()) && at_toplevel (mind_modpath kn)) || + kn_ord (canonical_mind kn) (user_mind kn) = 0 + then NoEquiv else begin @@ -381,8 +386,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ip_logical = (not b); ip_sign = s; ip_vars = v; - ip_types = t; - ip_optim_id_ok = None }) + ip_types = t }) mib.mind_packets in diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 0bf1ff952..5a19cc3f5 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. *) |