From c57c7edbe517851c7309112f6eb5d8297f03e000 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Jul 2015 17:36:58 +0200 Subject: Univs/Inductive: fix typechecking of cases I was trying to be a bit too clever with not substituting the universe instance everywhere: the constructor type/inductive arity has to be instantiated before instantiate_params runs, which became true only for constructor types since my last commit. --- kernel/inductive.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cf4177c50..87c139f48 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -93,7 +93,7 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = prop_sort in - let t = mkArity (sign,dummy) in + let t = mkArity (Vars.subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = @@ -344,13 +344,13 @@ let is_correct_arity env c pj ind specif params = | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (na1,None,a1) env in let ksort = match kind_of_term (whd_betadeltaiota env' a2) with - | Sort s -> family_of_sort s - | _ -> raise (LocalArity None) in + | Sort s -> family_of_sort s + | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in let _ = try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None) in - check_allowed_sort ksort specif + check_allowed_sort ksort specif | _, (_,Some _,_ as d)::ar' -> srec (push_rel d env) (lift 1 pt') ar' | _ -> -- cgit v1.2.3