diff options
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 27 |
1 files changed, 19 insertions, 8 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 55475a378..e17038a4f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -69,23 +69,34 @@ let abstract_inductive hyps nparams inds = in (params',ind'') let refresh_polymorphic_type_of_inductive (_,mip) = - mip.mind_arity.mind_user_arity + match mip.mind_arity with + | RegularArity s -> s.mind_user_arity, Univ.ContextSet.empty + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let univ, uctx = Universes.new_global_univ () in + mkArity (List.rev ctx, Type univ), uctx let process_inductive (sechyps,abs_ctx) modlist mib = let nparams = mib.mind_nparams in + let univctx = ref Univ.ContextSet.empty in let inds = Array.map_to_list (fun mip -> - let arity = expmod_constr modlist (refresh_polymorphic_type_of_inductive (mib,mip)) in - let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in - (mip.mind_typename, - arity, - Array.to_list mip.mind_consnames, - Array.to_list lc)) + let ty, uctx = refresh_polymorphic_type_of_inductive (mib,mip) in + let () = univctx := Univ.ContextSet.union uctx !univctx in + let arity = expmod_constr modlist ty in + let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in + (mip.mind_typename, + arity, + Array.to_list mip.mind_consnames, + Array.to_list lc)) 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 + (Univ.UContext.union (Univ.ContextSet.to_context !univctx) + mib.mind_universes) + in { mind_entry_record = mib.mind_record <> None; mind_entry_finite = mib.mind_finite; mind_entry_params = params'; |