diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 10 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 6 |
2 files changed, 9 insertions, 7 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 95341307a3..63c2dde182 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -849,7 +849,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 @@ -857,7 +857,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 @@ -1391,7 +1393,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; @@ -1408,7 +1410,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; diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 29f57144a9..ac6d775e34 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -24,14 +24,14 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - Typeops.check_hyps_inclusion env (mkInd ind) mib.mind_hyps; + Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps; Inductive.type_of_inductive env (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps; + Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif (* Return constructor types in user form *) @@ -615,7 +615,7 @@ let type_of_projection_knowing_arg env sigma p c ty = raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type") in let (_,u), pars = dest_ind_family pars in - substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u)) + substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u)) (***********************************************) (* Guard condition *) |