diff options
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 51 |
1 files changed, 31 insertions, 20 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 366f504545..63ca227862 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -265,16 +265,10 @@ let warn_non_primitive_record = let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in - let paramdecls = Inductive.inductive_paramdecls (mib, u) in let poly = Declareops.inductive_is_polymorphic mib in - let ctx = - match mib.mind_universes with - | Monomorphic_ind ctx -> ctx - | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx - | Cumulative_ind cumi -> - Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) - in + let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in + let u = Univ.UContext.instance ctx in + let paramdecls = Inductive.inductive_paramdecls (mib, u) in let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in @@ -334,8 +328,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; - const_entry_universes = - if poly then ctx else Univ.UContext.empty; + const_entry_universes = ctx; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -431,6 +424,12 @@ let declare_structure finite univs id idbuild paramimpls params arity template let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in + let fields = + if poly then + let subst, _ = Univ.abstract_universes ctx in + Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields + else fields + in let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in @@ -518,8 +517,18 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity | None -> None) params, params in + let univs, ctx_context, fields = + if poly then + let usubst, auctx = Univ.abstract_universes ctx in + let map c = Vars.subst_univs_level_constr usubst c in + let fields = Context.Rel.map map fields in + let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in + auctx, ctx_context, fields + else Univ.AUContext.empty, ctx_context, fields + in let k = - { cl_impl = impl; + { cl_univs = univs; + cl_impl = impl; cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique; cl_context = ctx_context; @@ -530,10 +539,11 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity let add_constant_class cst = - let ty = Universes.unsafe_type_of_global (ConstRef cst) in + let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in let ctx, arity = decompose_prod_assum ty in let tc = - { cl_impl = ConstRef cst; + { cl_univs = univs; + cl_impl = ConstRef cst; cl_context = (List.map (const None) ctx, ctx); cl_props = [LocalAssum (Anonymous, arity)]; cl_projs = []; @@ -547,12 +557,13 @@ let add_inductive_class ind = let mind, oneind = Global.lookup_inductive ind in let k = let ctx = oneind.mind_arity_ctxt in - let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in - let ty = Inductive.type_of_inductive - (push_rel_context ctx (Global.env ())) - ((mind,oneind),inst) - in - { cl_impl = IndRef ind; + let univs = Declareops.inductive_polymorphic_context mind in + let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in + let env = push_rel_context ctx env in + let inst = Univ.make_abstract_instance univs in + let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in + { cl_univs = univs; + cl_impl = IndRef ind; cl_context = List.map (const None) ctx, ctx; cl_props = [LocalAssum (Anonymous, ty)]; cl_projs = []; |