diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-01-22 10:52:18 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-01-22 12:05:10 +0100 |
commit | e91ae93106b6bd6d92ef53ac18b04654485a8106 (patch) | |
tree | 30bfa5ada3f09a639f78130b0d5518ff4f266abe /pretyping/cases.ml | |
parent | 6ff62ec78d5517ec5905041fa2e4926e15ff89f0 (diff) |
Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).
A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.
This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.
Thanks to Jason for helping in diagnosing the problem.
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r-- | pretyping/cases.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6e4d72705..ef3e53bf1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -847,7 +847,7 @@ let subst_predicate (subst,copt) ccl tms = | Some c -> c::subst in substnl_predicate sigma 0 ccl tms -let specialize_predicate_var (cur,typ,dep) tms ccl = +let specialize_predicate_var (cur,typ,dep) env tms ccl = let c = match dep with | Anonymous -> None | Name _ -> Some cur @@ -855,7 +855,9 @@ let specialize_predicate_var (cur,typ,dep) tms ccl = let l = match typ with | IsInd (_, IndType (_, _), []) -> [] - | IsInd (_, IndType (_, realargs), names) -> realargs + | IsInd (_, IndType (indf, realargs), names) -> + let arsign,_ = get_arity env indf in + subst_of_rel_context_instance arsign realargs | NotInd _ -> [] in subst_predicate (l,c) ccl tms @@ -1390,7 +1392,7 @@ and match_current pb (initial,tomatch) = and shift_problem ((current,t),_,na) pb = let ty = type_of_tomatch t in let tomatch = lift_tomatch_stack 1 pb.tomatch in - let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in + let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in let pb = { pb with env = push_rel (LocalDef (na,current,ty)) pb.env; @@ -1407,7 +1409,7 @@ and shift_problem ((current,t),_,na) pb = are already introduced in the context, we avoid creating aliases to themselves by treating this case specially. *) and pop_problem ((current,t),_,na) pb = - let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in + let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in let pb = { pb with pred = pred; |