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

5 files changed, 16 insertions, 12 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 1d1383f60f..1f6a07a6df 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -112,7 +112,8 @@ let contents_first_level mp =
 		      | Extraction.Term -> add false (id_of_label l))
 	       | (_, SPBmind mib) ->
 		   Array.iter 
-		     (fun mip -> if mip.mind_sort <> (Prop Null) then begin
+		     (fun mip -> if snd (Inductive.mind_arity mip) <> InProp
+		      then begin
 			add upper_type mip.mind_typename; 
 			Array.iter (add true) mip.mind_consnames
 		      end)
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0485c13688..485b75b9f2 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))
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 21f977f1c0..9e45006865 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -86,7 +86,7 @@ let rec def_const_in_term_rec vl x =
    | Sort(c) -> c
    | Ind(ind) ->
           let (mib, mip) = Global.lookup_inductive ind in
-          mip.mind_sort
+	  new_sort_in_family (inductive_sort_family mip)
    | Construct(c) ->
           def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
    | Case(_,x,t,a) 
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index b7da5c1b76..ce2ee1e7da 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -719,7 +719,7 @@ let rec nsortrec vl x =
    | Sort(c) -> c
    | Ind(ind) ->
           let (mib,mip) = lookup_mind_specif vl ind in
-          mip.mind_sort
+	  new_sort_in_family (inductive_sort_family mip)
    | Construct(c) ->
           nsortrec vl (mkInd (inductive_of_constructor c))
    | Case(_,x,t,a) 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 871a7f15cb..2235be4a08 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -395,7 +395,7 @@ let mk_constant_obj id bo ty variables hyps =
          ty,params)
 ;;
 
-let mk_inductive_obj sp packs variables nparams hyps finite =
+let mk_inductive_obj sp mib packs variables nparams hyps finite =
  let module D = Declarations in
   let hyps = string_list_of_named_context_list hyps in
   let params = filter_params variables hyps in
@@ -406,9 +406,9 @@ let mk_inductive_obj sp packs variables nparams hyps finite =
      (fun p i ->
        decr tyno ;
        let {D.mind_consnames=consnames ;
-            D.mind_typename=typename ;
-            D.mind_nf_arity=arity} = p
+            D.mind_typename=typename } = p
        in
+        let arity = Inductive.type_of_inductive (mib,p) in
         let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
         let cons =
          (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
@@ -524,11 +524,12 @@ let print internal glob_ref kind xml_library_root =
         G.lookup_constant kn in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->
+       let mib = G.lookup_mind kn in
        let {D.mind_nparams=nparams;
 	    D.mind_packets=packs ;
             D.mind_hyps=hyps;
-            D.mind_finite=finite} = G.lookup_mind kn in
-          Cic2acic.Inductive kn,mk_inductive_obj kn packs variables nparams hyps finite
+            D.mind_finite=finite} = mib in
+          Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
     | Ln.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in