From 70102c9c7b059b6a058e14c4cfda9cdd29ee3010 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Mar 2000 00:03:56 +0000
Subject: 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
---
 kernel/typeops.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'kernel/typeops.ml')

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 }
 
-- 
cgit v1.2.3