diff options
Diffstat (limited to 'plugins')
| -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 549830fe7c..2ab5bf9bf8 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 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. *) |