diff options
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index bd5218eff..971ae70d8 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -77,12 +77,23 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let process_inductive (sechyps,abs_ctx) modlist mib = let nparams = mib.mind_nparams in + let subst, univs = + if mib.mind_polymorphic then + let inst = Univ.UContext.instance mib.mind_universes in + let cstrs = Univ.UContext.constraints mib.mind_universes in + inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) + else Univ.Instance.empty, mib.mind_universes + in let inds = Array.map_to_list (fun mip -> let ty = refresh_polymorphic_type_of_inductive (mib,mip) in let arity = expmod_constr modlist ty in - let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in + let arity = Vars.subst_instance_constr subst arity in + let lc = Array.map + (fun c -> Vars.subst_instance_constr subst (expmod_constr modlist c)) + mip.mind_user_lc + in (mip.mind_typename, arity, Array.to_list mip.mind_consnames, @@ -90,7 +101,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mib.mind_packets in let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in - let univs = Univ.UContext.union abs_ctx mib.mind_universes in + let univs = Univ.UContext.union abs_ctx univs in let record = match mib.mind_record with | None -> None | Some (_, a) -> Some (Array.length a > 0) |