diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-08 21:34:26 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-08 21:34:26 +0000 |
commit | e4d70800bf92818b137fd91934cdf3c15844720d (patch) | |
tree | 657372c56fda9dab48d35dc0a57902beb5dc098b /pretyping | |
parent | aa85a3eddc2ebc908c210792fca948d927a0c871 (diff) |
MAJ nouveau try_mutind_of
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@304 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/retyping.ml | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 7d5417829..b84e1f0be 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -12,13 +12,6 @@ open Typeops type metamap = (int * constr) list -let rec is_dep_case env sigma (pt,ar) = - match whd_betadeltaiota env sigma pt,whd_betadeltaiota env sigma ar with - DOP2(Prod,_,DLAM(_,t1)),DOP2(Prod,_,DLAM(_,t2)) -> - is_dep_case env sigma (t1,t2) - | DOP2(Prod,_,DLAM(_,_)),ki -> true - | k,ki -> false - let outsort env sigma t = match whd_betadeltaiota env sigma t with DOP0(Sort s) -> s @@ -60,12 +53,13 @@ let rec type_of env cstr= | IsMutConstruct cstr -> let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ | IsMutCase (_,p,c,lf) -> - let {realargs=args;arity=arity;nparams=n} = + let {realargs=args;make_arity=make_arity;params=params;mind=mind} = try try_mutind_of env sigma (type_of env c) with Induc -> anomaly "type_of: Bad inductive" in - let (_,ar) = decomp_n_prod env sigma n arity in + let (aritysign,_) = make_arity mind params in + let (psign,_) = splay_prod env sigma (type_of env p) in let al = - if is_dep_case env sigma (type_of env p,ar) + if List.length psign > List.length aritysign then args@[c] else args in whd_betadeltaiota env sigma (applist (p,al)) | IsLambda (name,c1,c2) -> |