Nouvelle implantation du polymorphisme de sorte pour les familles inductives

- prise en compte du niveau à la déclaration du type comme une fonction
  des sortes des conclusions des paramètres uniformes
- suppression du retypage de chaque instance de type inductif (trop coûteux)
  et donc abandon de l'idée de calculer une sorte minimale même dans
  des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t.


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

1 files changed, 6 insertions, 4 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0485c1368..485b75b9f 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -316,9 +316,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     (* their type var list. *)
     let packets = 
       Array.map 
-	(fun mip -> 
-	   let b = mip.mind_sort <> (Prop Null) in 
-	   let s,v = if b then type_sign_vl env mip.mind_nf_arity else [],[] in
+	(fun mip ->
+	   let b = snd (mind_arity mip) <> InProp in
+	   let ar = Inductive.type_of_inductive (mib,mip) in
+	   let s,v = if b 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;
@@ -397,7 +398,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	(* Is this record officially declared with its projections ? *)
 	(* If so, we use this information. *)
 	begin try 
-	  let n = nb_default_params env mip0.mind_nf_arity in
+	  let n = nb_default_params env (Inductive.type_of_inductive(mib,mip0))
+	  in
 	  List.iter 
 	    (option_iter 
 	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))