Prise en compte nouveau case_info dans type_case

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

3 files changed, 9 insertions, 12 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ea6ce77aaa..0e855e443f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -67,12 +67,12 @@ let rec execute mf env cstr =
 	let (typ,kind) =destCast (type_of_constructor env Evd.empty c) in
         ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0)
 	  
-    | IsMutCase (_,p,c,lf) ->
+    | IsMutCase (ci,p,c,lf) ->
         let (cj,cst1) = execute mf env c in
         let (pj,cst2) = execute mf env p in
         let (lfj,cst3) = execute_array mf env lf in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
-        (type_of_case env Evd.empty pj cj lfj, cst)
+        (type_of_case env Evd.empty ci pj cj lfj, cst)
   
     | IsFix (vn,i,lar,lfi,vdef) ->
         if (not mf.fix) && array_exists (fun n -> n < 0) vn then
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 242641feff..c7496554c9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -170,11 +170,11 @@ let type_of_existential env sigma c =
 
 (* Case. *)
 
-let rec sort_of_arity env sigma c =
+let rec mysort_of_arity env sigma c =
   match whd_betadeltaiota env sigma c with
     | DOP0(Sort( _)) as c' -> c'
-    | DOP2(Prod,_,DLAM(_,c2)) -> sort_of_arity env sigma c2
-    | _ -> invalid_arg "sort_of_arity"
+    | DOP2(Prod,_,DLAM(_,c2)) -> mysort_of_arity env sigma c2
+    | _ -> invalid_arg "mysort_of_arity"
 
 let make_arity_dep env sigma k = 
   let rec mrec c m = match whd_betadeltaiota env sigma c with 
@@ -315,14 +315,13 @@ let check_branches_message env sigma (c,ct) (explft,lft) =
 	(nf_betaiota env sigma explft.(i))
   done
 
-let type_of_case env sigma pj cj lfj =
+let type_of_case env sigma ci pj cj lfj =
   let lft = Array.map (fun j -> j.uj_type) lfj in
   let (mind,bty,rslty) =
     type_case_branches env sigma cj.uj_type pj.uj_type pj.uj_val cj.uj_val in
-  let kind = sort_of_arity env sigma pj.uj_type in
+  let kind = mysort_of_arity env sigma pj.uj_type in
   check_branches_message env sigma (cj.uj_val,cj.uj_type) (bty,lft);
-  { uj_val  = 
-      mkMutCaseA (ci_of_mind mind) (j_val pj) (j_val cj) (Array.map j_val lfj);
+  { uj_val  = mkMutCaseA ci (j_val pj) (j_val cj) (Array.map j_val lfj);
     uj_type = rslty;
     uj_kind = kind }
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a7aec8cde5..90df90099b 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -35,9 +35,7 @@ val type_of_constructor : env -> 'a evar_map -> constructor -> constr
 
 val type_of_existential : env -> 'a evar_map -> constr -> constr
 
-val sort_of_arity : env -> 'a Evd.evar_map -> constr -> constr 
-
-val type_of_case : env -> 'a evar_map 
+val type_of_case : env -> 'a evar_map -> case_info
   -> unsafe_judgment -> unsafe_judgment 
     -> unsafe_judgment array -> unsafe_judgment