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

1 files changed, 10 insertions, 6 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