From 2f56532885d91b20b4c7b084abc4e49b82ab1c28 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 30 Nov 2011 16:38:11 +0000
Subject: 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
---
 plugins/extraction/extraction.ml | 16 ++++++++++------
 plugins/extraction/miniml.mli    |  3 +--
 2 files changed, 11 insertions(+), 8 deletions(-)

(limited to 'plugins')

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. *)
-- 
cgit v1.2.3