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, 3 insertions, 11 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 776f1313f..2fdb4148a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -118,17 +118,9 @@ let typeur sigma metamap =
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
   and type_of_applied_inductive env ind args =
-    let specif = lookup_mind_specif env ind in
-    let t = Inductive.type_of_inductive specif in
-    if is_small_inductive specif then
-      (* No polymorphism *)
-      t
-    else
-      (* Retyping constructor with the actual arguments *)
-      let env',llc,ls0 = constructor_instances env specif ind args in
-      let lls = Array.map (Array.map (sort_of env')) llc in
-      let ls = Array.map max_inductive_sort lls in
-      set_inductive_level env (find_inductive_level env specif ind ls0 ls) t
+    let (_,mip) = lookup_mind_specif env ind in
+    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
+    Inductive.type_of_applied_inductive env mip argtyps
 
   in type_of, sort_of, sort_family_of, type_of_applied_inductive