diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 26 |
1 files changed, 9 insertions, 17 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 32da4cea..428a7306 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retyping.ml 8673 2006-03-29 21:21:52Z herbelin $ *) +(* $Id: retyping.ml 8871 2006-05-28 16:46:48Z herbelin $ *) open Util open Term @@ -74,7 +74,7 @@ let typeur sigma metamap = | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) | App(f,args) when isInd f -> - let t = type_of_applied_inductive env (destInd f) args in + let t = type_of_inductive_knowing_parameters env (destInd f) args in strip_outer_cast (subst_type env sigma t (Array.to_list args)) | App(f,args) -> strip_outer_cast @@ -98,7 +98,7 @@ let typeur sigma metamap = | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) | App(f,args) when isInd f -> - let t = type_of_applied_inductive env (destInd f) args in + let t = type_of_inductive_knowing_parameters env (destInd f) args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | Lambda _ | Fix _ | Construct _ -> @@ -117,25 +117,17 @@ let typeur sigma metamap = anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) - and type_of_applied_inductive env ind args = - let specif = lookup_mind_specif env ind in - let t = Inductive.type_of_inductive specif in - if is_small_inductive specif then - (* No polymorphism *) - t - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let lls = Array.map (Array.map (sort_of env')) llc in - let ls = Array.map max_inductive_sort lls in - set_inductive_level env (find_inductive_level env specif ind ls0 ls) t + and type_of_inductive_knowing_parameters env ind args = + let (_,mip) = lookup_mind_specif env ind in + let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in + Inductive.type_of_inductive_knowing_parameters env mip argtyps - in type_of, sort_of, sort_family_of, type_of_applied_inductive + in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c -let type_of_applied_inductive env sigma ind args = +let type_of_inductive_knowing_parameters env sigma ind args = let _,_,_,f = typeur sigma [] in f env ind args let get_type_of_with_meta env sigma metamap = |