diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 2 | ||||
| -rw-r--r-- | vernac/discharge.ml | 16 | ||||
| -rw-r--r-- | vernac/record.ml | 8 | ||||
| -rw-r--r-- | vernac/record.mli | 2 |
4 files changed, 11 insertions, 17 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 5f95a42a3..b76c2247b 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = (uctx, Univ.UContext.empty); + mind_entry_universes = Universes.univ_inf_ind_from_universe_context uctx; }, pl, impls diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 9c70eb97e..91e126ef1 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -81,17 +81,10 @@ 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 + let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) in + let cstrs = Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes) in inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) - else Univ.Instance.empty, mib.mind_universes - in - let substsbt, univssbt = - if mib.mind_polymorphic then - let inst = Univ.UContext.instance mib.mind_subtyping in - let cstrs = Univ.UContext.constraints mib.mind_subtyping in - inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) - else Univ.Instance.empty, Univ.UContext.empty + else Univ.Instance.empty, (Univ.UInfoInd.univ_context mib.mind_universes) in let inds = Array.map_to_list @@ -112,6 +105,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = let (params',inds') = abstract_inductive sechyps' nparams inds in let abs_ctx = Univ.instantiate_univ_context abs_ctx in let univs = Univ.UContext.union abs_ctx univs in + let univ_info_ind = Universes.univ_inf_ind_from_universe_context univs in (* Here we must re-infer subtyping constraints. For now we just revert to trivial subtyping. *) let record = match mib.mind_record with | Some (Some (id, _, _)) -> Some (Some id) | Some None -> Some None @@ -123,5 +117,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = (univs, univssbt); + mind_entry_universes = univ_info_ind } diff --git a/vernac/record.ml b/vernac/record.ml index 5c76bb4b2..64f5e81d4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -268,7 +268,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let u = Declareops.inductive_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let poly = mib.mind_polymorphic in - let ctx = Univ.instantiate_univ_context mib.mind_universes in + let ctx = Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) 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 @@ -466,7 +466,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly (ctx, Univ.UContext.empty) (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -515,7 +515,7 @@ 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.UContext.instance mind.mind_universes in + let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) @@ -571,7 +571,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite poly (ctx, Univ.UContext.empty) idstruc + let ind = declare_structure finite poly (Universes.univ_inf_ind_from_universe_context ctx) idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind diff --git a/vernac/record.mli b/vernac/record.mli index a380b041a..ec5d2cf83 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -27,7 +27,7 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> bool (** polymorphic?*) -> - (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) -> + Univ.universe_info_ind (** universe and subtyping constraints *) -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> |