aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/uState.ml19
-rw-r--r--engine/univNames.ml17
-rw-r--r--engine/univNames.mli2
-rw-r--r--interp/declare.ml14
-rw-r--r--interp/discharge.ml6
-rw-r--r--interp/modintern.ml2
-rw-r--r--kernel/entries.ml6
-rw-r--r--kernel/indtypes.ml12
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/term_typing.ml8
-rw-r--r--kernel/univ.ml3
-rw-r--r--kernel/univ.mli3
-rw-r--r--pretyping/inferCumulativity.ml4
-rw-r--r--tactics/abstract.ml2
-rw-r--r--tactics/ind_tables.ml7
-rw-r--r--test-suite/misc/poly-capture-global-univs/src/evilImpl.ml2
-rw-r--r--vernac/classes.ml15
-rw-r--r--vernac/comAssumption.ml4
-rw-r--r--vernac/comInductive.ml6
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/obligations.ml7
-rw-r--r--vernac/record.ml27
22 files changed, 97 insertions, 73 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index aa7ec63a6f..41905feab7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -101,13 +101,21 @@ let context ctx = Univ.ContextSet.to_context ctx.uctx_local
let const_univ_entry ~poly uctx =
let open Entries in
- if poly then Polymorphic_const_entry (context uctx)
+ if poly then
+ let (binders, _) = uctx.uctx_names in
+ let uctx = context uctx in
+ let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+ Polymorphic_const_entry (nas, uctx)
else Monomorphic_const_entry (context_set uctx)
(* does not support cumulativity since you need more info *)
let ind_univ_entry ~poly uctx =
let open Entries in
- if poly then Polymorphic_ind_entry (context uctx)
+ if poly then
+ let (binders, _) = uctx.uctx_names in
+ let uctx = context uctx in
+ let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+ Polymorphic_ind_entry (nas, uctx)
else Monomorphic_ind_entry (context_set uctx)
let of_context_set ctx = { empty with uctx_local = ctx }
@@ -394,8 +402,11 @@ let check_univ_decl ~poly uctx decl =
let ctx =
let names = decl.univdecl_instance in
let extensible = decl.univdecl_extensible_instance in
- if poly
- then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+ if poly then
+ let (binders, _) = uctx.uctx_names in
+ let uctx = universe_context ~names ~extensible uctx in
+ let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+ Entries.Polymorphic_const_entry (nas, uctx)
else
let () = check_universe_context_set ~names ~extensible uctx in
Entries.Monomorphic_const_entry uctx.uctx_local
diff --git a/engine/univNames.ml b/engine/univNames.ml
index a71f9c5736..a037e577c4 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -81,18 +81,23 @@ let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
discharge_function = discharge_ubinder;
rebuild_function = (fun x -> x); }
+let compute_instance_binders inst ubinders =
+ let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
+ let map lvl =
+ try Name (LMap.find lvl revmap)
+ with Not_found -> Name (name_universe lvl)
+ in
+ Array.map_to_list map (Instance.to_array inst)
+
let register_universe_binders ref ubinders =
(** TODO: change the API to register a [Name.t list] instead. This is the last
part of the code that depends on the internal representation of names in
abstract contexts, but removing it requires quite a rework of the
callers. *)
let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
- let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
- let map lvl =
- try LMap.find lvl revmap
- with Not_found -> name_universe lvl
- in
- let ubinders = Array.map_to_list map (Instance.to_array univs) in
+ let ubinders = compute_instance_binders univs ubinders in
+ (** FIXME: the function above always generate names but this may change *)
+ let ubinders = List.map (function Name id -> id | Anonymous -> assert false) ubinders in
if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
type univ_name_list = Names.lname list
diff --git a/engine/univNames.mli b/engine/univNames.mli
index bd4062ade4..634db9581c 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,6 +19,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
val empty_binders : universe_binders
+val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list
+
val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
type univ_name_list = Names.lname list
diff --git a/interp/declare.ml b/interp/declare.ml
index 7a32018c0e..29e777d0c6 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -219,7 +219,7 @@ let cache_variable ((sp,_),o) =
let (body, uctx), () = Future.force de.const_entry_body in
let poly, univs = match de.const_entry_universes with
| Monomorphic_const_entry uctx -> false, uctx
- | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx
+ | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
in
let univs = Univ.ContextSet.union uctx univs in
(** We must declare the universe constraints before type-checking the
@@ -339,7 +339,7 @@ let infer_inductive_subtyping mind_ent =
match mind_ent.mind_entry_universes with
| Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
mind_ent
- | Cumulative_ind_entry cumi ->
+ | Cumulative_ind_entry (_, cumi) ->
begin
let env = Global.env () in
(* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
@@ -366,14 +366,14 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
| Monomorphic_ind_entry _ ->
(** Global constraints already defined through the inductive *)
Monomorphic_const_entry Univ.ContextSet.empty
- | Polymorphic_ind_entry ctx ->
- Polymorphic_const_entry ctx
- | Cumulative_ind_entry ctx ->
- Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+ | Polymorphic_ind_entry (nas, ctx) ->
+ Polymorphic_const_entry (nas, ctx)
+ | Cumulative_ind_entry (nas, ctx) ->
+ Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx)
in
let term, types = match univs with
| Monomorphic_const_entry _ -> term, types
- | Polymorphic_const_entry ctx ->
+ | Polymorphic_const_entry (_, ctx) ->
let u = Univ.UContext.instance ctx in
Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
in
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 21b2e85e8f..eeda5a6867 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -79,13 +79,15 @@ let process_inductive info modlist mib =
| Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
| Polymorphic_ind auctx ->
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+ let nas = Univ.AUContext.names auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Polymorphic_ind_entry auctx
+ subst, Polymorphic_ind_entry (nas, auctx)
| Cumulative_ind cumi ->
let auctx = Univ.ACumulativityInfo.univ_context cumi in
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+ let nas = Univ.AUContext.names auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
+ subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx)
in
let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
let inds =
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 51e27299e3..93aa271e8b 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,7 +107,7 @@ let transl_with_decl env base kind = function
let c, ectx = interp_constr env sigma c in
let poly = lookup_polymorphism env base kind fqid in
begin match UState.check_univ_decl ~poly ectx udecl with
- | Entries.Polymorphic_const_entry ctx ->
+ | Entries.Polymorphic_const_entry (nas, ctx) ->
let inst, ctx = Univ.abstract_universes ctx in
let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
let c = EConstr.to_constr sigma c in
diff --git a/kernel/entries.ml b/kernel/entries.ml
index c5bcd74072..87fa385a60 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
type inductive_universes =
| Monomorphic_ind_entry of Univ.ContextSet.t
- | Polymorphic_ind_entry of Univ.UContext.t
- | Cumulative_ind_entry of Univ.CumulativityInfo.t
+ | Polymorphic_ind_entry of Name.t list * Univ.UContext.t
+ | Cumulative_ind_entry of Name.t list * Univ.CumulativityInfo.t
type one_inductive_entry = {
mind_entry_typename : Id.t;
@@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
type constant_universes_entry =
| Monomorphic_const_entry of Univ.ContextSet.t
- | Polymorphic_const_entry of Univ.UContext.t
+ | Polymorphic_const_entry of Name.t list * Univ.UContext.t
type 'a in_constant_universes_entry = 'a * constant_universes_entry
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0346026aa4..2d74f99c15 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -268,8 +268,8 @@ let typecheck_inductive env mie =
let env' =
match mie.mind_entry_universes with
| Monomorphic_ind_entry ctx -> push_context_set ctx env
- | Polymorphic_ind_entry ctx -> push_context ctx env
- | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+ | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
+ | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
in
let env_params = check_context env' mie.mind_entry_params in
let paramsctxt = mie.mind_entry_params in
@@ -407,7 +407,7 @@ let typecheck_inductive env mie =
match mie.mind_entry_universes with
| Monomorphic_ind_entry _ -> ()
| Polymorphic_ind_entry _ -> ()
- | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds
+ | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds
in (env_arities, env_ar_par, paramsctxt, inds)
(************************************************************************)
@@ -851,12 +851,14 @@ let compute_projections (kn, i as ind) mib =
let abstract_inductive_universes iu =
match iu with
| Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
- | Polymorphic_ind_entry ctx ->
+ | Polymorphic_ind_entry (nas, ctx) ->
+ let () = assert (Int.equal (List.length nas) (UContext.size ctx)) in
let (inst, auctx) = Univ.abstract_universes ctx in
let inst = Univ.make_instance_subst inst in
(inst, Polymorphic_ind auctx)
- | Cumulative_ind_entry cumi ->
+ | Cumulative_ind_entry (nas, cumi) ->
let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+ let () = assert (Int.equal (List.length nas) (Instance.length inst)) in
let inst = Univ.make_instance_subst inst in
(inst, Cumulative_ind acumi)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8b11851bbb..df10398b2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -682,7 +682,7 @@ let constant_entry_of_side_effect cb u =
| Monomorphic_const uctx ->
Monomorphic_const_entry uctx
| Polymorphic_const auctx ->
- Polymorphic_const_entry (Univ.AUContext.repr auctx)
+ Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
in
let pt =
match cb.const_body, u with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index fb1b3e236c..4759625e8a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,7 +68,8 @@ let feedback_completion_typecheck =
let abstract_constant_universes = function
| Monomorphic_const_entry uctx ->
Univ.empty_level_subst, Monomorphic_const uctx
- | Polymorphic_const_entry uctx ->
+ | Polymorphic_const_entry (nas, uctx) ->
+ let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in
let sbst, auctx = Univ.abstract_universes uctx in
let sbst = Univ.make_instance_subst sbst in
sbst, Polymorphic_const auctx
@@ -78,7 +79,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
| ParameterEntry (ctx,(t,uctx),nl) ->
let env = match uctx with
| Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
- | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+ | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
in
let j = infer env t in
let usubst, univs = abstract_constant_universes uctx in
@@ -150,7 +151,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let ctx = Univ.ContextSet.union univs ctx in
let env = push_context_set ~strict:true ctx env in
env, Univ.empty_level_subst, Monomorphic_const ctx
- | Polymorphic_const_entry uctx ->
+ | Polymorphic_const_entry (nas, uctx) ->
(** Ensure not to generate internal constraints in polymorphic mode.
The only way for this to happen would be that either the body
contained deferred universes, or that it contains monomorphic
@@ -159,6 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
unconditionally export side-effects from polymorphic definitions,
i.e. [trust] is always [Pure]. *)
let () = assert (Univ.ContextSet.is_empty ctx) in
+ let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in
let env = push_context ~strict:false uctx env in
let sbst, auctx = Univ.abstract_universes uctx in
let sbst = Univ.make_instance_subst sbst in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d09b54e7ec..35566019a8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -948,6 +948,9 @@ struct
assert (Array.length u = Array.length inst);
subst_instance_constraints inst cst
+ (** FIXME: Actually store this information in the type *)
+ let names (u, _) = Array.map_to_list (fun _ -> Names.Anonymous) u
+
end
let hcons_abstract_universe_context = AUContext.hcons
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7ac8247ca4..bc902d8f4b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -347,6 +347,9 @@ sig
val instantiate : Instance.t -> t -> Constraint.t
(** Generate the set of instantiated Constraint.t **)
+ val names : t -> Names.Name.t list
+ (** Return the names of the bound universe variables *)
+
end
(** Universe info for cumulative inductive types: A context of
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index 422a05c19a..9762d0f1d9 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -188,7 +188,7 @@ let infer_inductive env mie =
match mie.mind_entry_universes with
| Monomorphic_ind_entry _
| Polymorphic_ind_entry _ as univs -> univs
- | Cumulative_ind_entry cumi ->
+ | Cumulative_ind_entry (nas, cumi) ->
let uctx = CumulativityInfo.univ_context cumi in
let uarray = Instance.to_array @@ UContext.instance uctx in
let env = Environ.push_context uctx env in
@@ -207,6 +207,6 @@ let infer_inductive env mie =
entries
in
let variances = Array.map (fun u -> LMap.find u variances) uarray in
- Cumulative_ind_entry (CumulativityInfo.make (uctx, variances))
+ Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances))
in
{ mie with mind_entry_universes = univs }
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 2b4d9a7adf..3c262de910 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -148,7 +148,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let cst = Impargs.with_implicit_protection cst () in
let inst = match const.Entries.const_entry_universes with
| Entries.Monomorphic_const_entry _ -> EInstance.empty
- | Entries.Polymorphic_const_entry ctx ->
+ | Entries.Polymorphic_const_entry (_, ctx) ->
(** We mimick what the kernel does, that is ensuring that no additional
constraints appear in the body of polymorphic constants. Ideally this
should be enforced statically. *)
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index b81967c781..a53e3bf20d 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -118,15 +118,12 @@ let compute_name internal id =
| InternalTacticRequest ->
Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
-let define internal id c p univs =
+let define internal id c poly univs =
let fd = declare_constant ~internal in
let id = compute_name internal id in
let ctx = UState.minimize univs in
let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
- let univs =
- if p then Polymorphic_const_entry (UState.context ctx)
- else Monomorphic_const_entry (UState.context_set ctx)
- in
+ let univs = UState.const_univ_entry ~poly ctx in
let entry = {
const_entry_body =
Future.from_val ((c,Univ.ContextSet.empty),
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index 6d8ce7c5d7..c4b36fb9e0 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -15,7 +15,7 @@ let evil t f =
let tc = mkConst tc in
let fe = Declare.definition_entry
- ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty)))
+ ~univs:(Polymorphic_const_entry ([Anonymous], UContext.make (Instance.of_array [|u|],Constraint.empty)))
~types:(Term.mkArrow tc tu)
(mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index f4b0015851..3bac4a6555 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -370,25 +370,24 @@ let context poly l =
user_err Pp.(str "Anonymous variables not allowed in contexts.")
in
let univs =
- let uctx = Evd.universe_context_set sigma in
match ctx with
| [] -> assert false
- | [_] ->
- if poly
- then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
- else Monomorphic_const_entry uctx
+ | [_] -> Evd.const_univ_entry ~poly sigma
| _::_::_ ->
+ (** TODO: explain this little belly dance *)
if Lib.sections_are_opened ()
then
begin
+ let uctx = Evd.universe_context_set sigma in
Declare.declare_universe_context poly uctx;
- if poly then Polymorphic_const_entry Univ.UContext.empty
+ if poly then Polymorphic_const_entry ([], Univ.UContext.empty)
else Monomorphic_const_entry Univ.ContextSet.empty
end
- else if poly
- then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
+ else if poly then
+ Evd.const_univ_entry ~poly sigma
else
begin
+ let uctx = Evd.universe_context_set sigma in
Declare.declare_universe_context poly uctx;
Monomorphic_const_entry Univ.ContextSet.empty
end
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e990f0cd15..8707121306 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -47,7 +47,7 @@ match local with
| Discharge when Lib.sections_are_opened () ->
let ctx = match ctx with
| Monomorphic_const_entry ctx -> ctx
- | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx
+ | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx
in
let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
let _ = declare_variable ident decl in
@@ -79,7 +79,7 @@ match local with
let () = if do_instance then Typeclasses.declare_instance None false gr in
let () = if is_coe then Class.try_add_new_coercion gr ~local p in
let inst = match ctx with
- | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+ | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
| Monomorphic_const_entry _ -> Univ.Instance.empty
in
(gr,inst,Lib.is_modtype_strict ())
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5ff3032ec4..0c39458a57 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -450,10 +450,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
in
let univs =
match uctx with
- | Polymorphic_const_entry uctx ->
+ | Polymorphic_const_entry (nas, uctx) ->
if cum then
- Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx)
- else Polymorphic_ind_entry uctx
+ Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx)
+ else Polymorphic_ind_entry (nas, uctx)
| Monomorphic_const_entry uctx ->
Monomorphic_ind_entry uctx
in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8aa459729c..602314eec3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -228,7 +228,7 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
| Discharge ->
let impl = false in (* copy values from Vernacentries *)
let univs = match univs with
- | Polymorphic_const_entry univs ->
+ | Polymorphic_const_entry (_, univs) ->
(* What is going on here? *)
Univ.ContextSet.of_context univs
| Monomorphic_const_entry univs -> univs
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 97ed43c5f4..c2805674e4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -667,7 +667,7 @@ let declare_obligation prg obl body ty uctx =
if not opaque then add_hint (Locality.make_section_locality None) prg constant;
definition_message obl.obl_name;
let body = match uctx with
- | Polymorphic_const_entry uctx ->
+ | Polymorphic_const_entry (_, uctx) ->
Some (DefinedObl (constant, Univ.UContext.instance uctx))
| Monomorphic_const_entry _ ->
Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
@@ -1004,10 +1004,7 @@ and solve_obligation_by_tac prg obls i tac =
solve_by_tac obl.obl_name (evar_of_obligation obl) tac
(pi2 prg.prg_kind) (Evd.evar_universe_context evd)
in
- let uctx = if pi2 prg.prg_kind
- then Polymorphic_const_entry (UState.context ctx)
- else Monomorphic_const_entry (UState.context_set ctx)
- in
+ let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
let prg = {prg with prg_ctx = ctx} in
let def, obl' = declare_obligation prg obl t ty uctx in
obls.(i) <- obl';
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a4c38e972..5b3fb81d66 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -282,7 +282,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
let (mib,mip) = Global.lookup_inductive indsp in
let poly = Declareops.inductive_is_polymorphic mib in
let u = match ctx with
- | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+ | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
| Monomorphic_const_entry ctx -> Univ.Instance.empty
in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
@@ -389,10 +389,10 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
match univs with
| Monomorphic_ind_entry ctx ->
false, Monomorphic_const_entry Univ.ContextSet.empty
- | Polymorphic_ind_entry ctx ->
- true, Polymorphic_const_entry ctx
- | Cumulative_ind_entry cumi ->
- true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+ | Polymorphic_ind_entry (nas, ctx) ->
+ true, Polymorphic_const_entry (nas, ctx)
+ | Cumulative_ind_entry (nas, cumi) ->
+ true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi)
in
let binder_name =
match name with
@@ -480,7 +480,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
(DefinitionEntry class_entry, IsDefinition Definition)
in
let inst, univs = match univs with
- | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs
+ | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs
| Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
in
let cstu = (cst, inst) in
@@ -508,11 +508,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
| _ ->
let univs =
match univs with
- | Polymorphic_const_entry univs ->
+ | Polymorphic_const_entry (nas, univs) ->
if cum then
- Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
+ Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
else
- Polymorphic_ind_entry univs
+ Polymorphic_ind_entry (nas, univs)
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
@@ -541,7 +541,8 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
in
let univs, ctx_context, fields =
match univs with
- | Polymorphic_const_entry univs ->
+ | Polymorphic_const_entry (nas, univs) ->
+ let () = assert (Int.equal (List.length nas) (Univ.UContext.size univs)) in
let usubst, auctx = Univ.abstract_universes univs in
let usubst = Univ.make_instance_subst usubst in
let map c = Vars.subst_univs_level_constr usubst c in
@@ -682,11 +683,11 @@ let definition_structure udecl kind ~template cum poly finite records =
let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
let univs =
match univs with
- | Polymorphic_const_entry univs ->
+ | Polymorphic_const_entry (nas, univs) ->
if cum then
- Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
+ Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
else
- Polymorphic_ind_entry univs
+ Polymorphic_ind_entry (nas, univs)
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:41:27 +0000