Fix extraction of inductive types that Coq auto-detects to be in Prop

 Typical example :

   Inductive t := T : t -> t.

 Earlier, the extraction was using a shortcut to get the sort of t
 (via some mind_arity stuff), but this was producing a less precise
 answer (here InType) than a full Retyping.get_sort_family_of
 (here InProp since t is a singleton type, with no content).
 The extraction of t was hence awkward, since the type of the
 constructor T was computed with the precise method, and its argument
 was optimized out. Now the whole t is considered logical by the
 extraction.

 NB: to avoid this clever but highly non-intuitive behavior of Coq placing
 the above t in Prop, for the moment you have to fix its sort, for instance:

  Inductive t : Set := T : t -> t.

 Using Type instead of Set still activates Coq's minimal sort detection...
 Instead, you could also use one specific TypeX obtained via
 Definition TypeX := Type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16203 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5ab3647d6..75c0374cf 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -373,15 +373,15 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     let packets =
-      Array.map
-	(fun mip ->
-	   let b = snd (mind_arity mip) <> InProp in
+      Array.mapi
+	(fun i mip ->
+	   let info = sort_of env (mkInd (kn,i)) <> InProp in
 	   let ar = Inductive.type_of_inductive env (mib,mip) in
-	   let s,v = if b then type_sign_vl env ar else [],[] in
+	   let s,v = if info then type_sign_vl env ar else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in
 	   { ip_typename = mip.mind_typename;
 	     ip_consnames = mip.mind_consnames;
-	     ip_logical = (not b);
+	     ip_logical = not info;
 	     ip_sign = s;
 	     ip_vars = v;
 	     ip_types = t })