diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index dfdc24d4..cb091f2d 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -322,7 +322,8 @@ let instantiate_params t args sign = let get_constructor ((ind,u as indu),mib,mip,params) j = assert (j <= Array.length mip.mind_consnames); let typi = mis_nf_constructor_type (indu,mib,mip) j in - let typi = instantiate_params typi params mib.mind_params_ctxt in + let ctx = Vars.subst_instance_context u mib.mind_params_ctxt in + let typi = instantiate_params typi params ctx in let (args,ccl) = decompose_prod_assum typi in let (_,allargs) = decompose_app ccl in let vargs = List.skipn (List.length params) allargs in @@ -584,6 +585,15 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = env evdref scl ar.template_level (ctx,ar.template_param_levels) in !evdref, mkArity (List.rev ctx,scl) +let type_of_projection_knowing_arg env sigma p c ty = + let IndType(pars,realargs) = + try find_rectype env sigma ty + with Not_found -> + 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)) + (***********************************************) (* Guard condition *) |