Un cast inutile

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

1 files changed, 1 insertions, 5 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f546c1081..242641fef 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -244,15 +244,11 @@ let is_correct_arity env sigma kelim (c,p) =
   in 
   srec 
 
-let cast_instantiate_arity mis =
-  let tty = instantiate_arity mis in
-  DOP2 (Cast, tty.body, DOP0 (Sort tty.typ))
-
 let find_case_dep_nparams env sigma (c,p) (mind,largs) typP =    
   let mis = lookup_mind_specif mind env in 
   let nparams = mis_nparams mis
   and kelim = mis_kelim mis 
-  and t = cast_instantiate_arity mis in 
+  and t = body_of_type (instantiate_arity mis) in 
   let (globargs,la) = list_chop nparams largs in
   let glob_t = hnf_prod_applist env sigma "find_elim_boolean" t globargs in
   let arity = applist(mkMutInd mind,globargs) in