From ff9a59ac99ea7a58c2be0a96a6b6b1482a592b2a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 17 Mar 2000 18:52:27 +0000
Subject: Un cast inutile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@321 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f546c1081b..242641feff 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
-- 
cgit v1.2.3