Précalcul de la forme canonique des constructeurs et arités pour traiter les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois

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

1 files changed, 20 insertions, 2 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 979d24536..197f5c299 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -315,12 +315,30 @@ let cci_inductive env env_ar kind nparams finite inds cst =
     let recargs = listrec_mconstr env_ar ntypes nparams i lc in
     let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
     let (ar_sign,ar_sort) = splay_arity env Evd.empty (body_of_type ar) in
+    let nf_ar,user_ar =
+      if isArity (body_of_type ar) then ar,None
+      else 
+	(make_typed_lazy (prod_it (mkSort ar_sort) ar_sign)
+	   (fun _ -> level_of_type ar)),
+	Some (body_of_type ar) in
     let kelim = allowed_sorts issmall isunit ar_sort in
+    let lc_bodies = Array.map body_of_type lc in
+    let splayed_lc = Array.map (splay_prod env Evd.empty) lc_bodies in
+    let nf_lc = Array.map (fun (d,b) -> prod_it b d) splayed_lc in
+    let nf_typed_lc,user_lc =
+      if nf_lc = lc_bodies then lc,None
+      else
+	(array_map2
+	   (fun nfc c -> make_typed_lazy nfc (fun _ -> level_of_type c))
+	   nf_lc lc),
+        Some lc_bodies in
     { mind_consnames = Array.of_list cnames;
       mind_typename = id;
-      mind_lc = lc;
+      mind_user_lc = user_lc;
+      mind_nf_lc = nf_typed_lc;
+      mind_user_arity  = user_ar;
+      mind_nf_arity = nf_ar;
       mind_nrealargs = List.length ar_sign - nparams;
-      mind_arity  = ar;
       mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_listrec = recargs;