diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-07-15 17:36:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-07-15 17:36:58 +0200 |
| commit | c57c7edbe517851c7309112f6eb5d8297f03e000 (patch) | |
| tree | 03b6da5a2f3719949e6f293e65ed7d653d3df264 | |
| parent | 44f3c1b1071506bcd98dec4e10675624c0142c21 (diff) | |
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.
| -rw-r--r-- | checker/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 00d3bc8e1..21b80f323 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -103,7 +103,7 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in - let t = mkArity (sign,dummy) in + let t = mkArity (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 = 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' | _ -> |