Extraction: same as commit 16203, hopefully without NotASort exns

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

1 files changed, 1 insertions, 1 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 75c0374cf9..62ce3f31d8 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -375,8 +375,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     let packets =
       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 info = (fst (flag_of_type env ar) = Info) 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;