aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli5
-rw-r--r--engine/universes.ml12
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/declareops.ml7
-rw-r--r--kernel/entries.mli2
-rw-r--r--kernel/indtypes.ml14
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/term_typing.ml2
-rw-r--r--kernel/univ.ml8
-rw-r--r--kernel/vconv.ml2
-rw-r--r--library/declare.ml2
-rw-r--r--library/global.ml12
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/vnorm.ml2
-rw-r--r--printing/printer.ml7
-rw-r--r--printing/printer.mli1
-rw-r--r--printing/printmod.ml10
-rw-r--r--vernac/command.ml2
-rw-r--r--vernac/discharge.ml16
-rw-r--r--vernac/record.ml8
-rw-r--r--vernac/record.mli2
22 files changed, 60 insertions, 64 deletions
diff --git a/API/API.mli b/API/API.mli
index e2c43dab8..cea879ba3 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -86,6 +86,8 @@ sig
type universe_context = UContext.t
[@@ocaml.deprecated "alias of API.Names.UContext.t"]
+ type universe_info_ind = Univ.UInfoInd.t
+
module LSet : module type of struct include Univ.LSet end
module ContextSet :
sig
@@ -1093,8 +1095,7 @@ sig
mind_nparams_rec : int;
mind_params_ctxt : Context.Rel.t;
mind_polymorphic : bool;
- mind_universes : Univ.UContext.t;
- mind_subtyping : Univ.universe_context;
+ mind_universes : Univ.universe_info_ind;
mind_private : bool option;
mind_typing_flags : Declarations.typing_flags;
}
diff --git a/engine/universes.ml b/engine/universes.ml
index 955e1d8b5..ad53bf898 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -338,14 +338,14 @@ let fresh_constant_instance env c inst =
let fresh_inductive_instance env ind inst =
let mib, mip = Inductive.lookup_mind_specif env ind in
if mib.Declarations.mind_polymorphic then
- let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in
+ let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) inst in
((ind,inst), ctx)
else ((ind,Instance.empty), ContextSet.empty)
let fresh_constructor_instance env (ind,i) inst =
let mib, mip = Inductive.lookup_mind_specif env ind in
if mib.Declarations.mind_polymorphic then
- let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in
+ let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) inst in
(((ind,i),inst), ctx)
else (((ind,i),Instance.empty), ContextSet.empty)
@@ -360,14 +360,14 @@ let unsafe_constant_instance env c =
let unsafe_inductive_instance env ind =
let mib, mip = Inductive.lookup_mind_specif env ind in
if mib.Declarations.mind_polymorphic then
- let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in
+ let inst, ctx = unsafe_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
((ind,inst), ctx)
else ((ind,Instance.empty), UContext.empty)
let unsafe_constructor_instance env (ind,i) =
let mib, mip = Inductive.lookup_mind_specif env ind in
if mib.Declarations.mind_polymorphic then
- let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in
+ let inst, ctx = unsafe_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
(((ind,i),inst), ctx)
else (((ind,i),Instance.empty), UContext.empty)
@@ -460,7 +460,7 @@ let type_of_reference env r =
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
if mib.mind_polymorphic then
- let inst, ctx = fresh_instance_from mib.mind_universes None in
+ let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.mind_universes) None in
let ty = Inductive.type_of_inductive env (specif, inst) in
ty, ctx
else
@@ -469,7 +469,7 @@ let type_of_reference env r =
| ConstructRef cstr ->
let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
if mib.mind_polymorphic then
- let inst, ctx = fresh_instance_from mib.mind_universes None in
+ let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.mind_universes) None in
Inductive.type_of_constructor (cstr,inst) specif, ctx
else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9536407d3..1bb1e885f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -188,9 +188,7 @@ type mutual_inductive_body = {
mind_polymorphic : bool; (** Is it polymorphic or not *)
- mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
-
- mind_subtyping : Univ.universe_context; (** Constraints for subtyping *)
+ mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 47a23c855..cdea468ad 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -261,19 +261,18 @@ let subst_mind_body sub mib =
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_polymorphic = mib.mind_polymorphic;
mind_universes = mib.mind_universes;
- mind_subtyping = mib.mind_subtyping;
mind_private = mib.mind_private;
mind_typing_flags = mib.mind_typing_flags;
}
let inductive_instance mib =
if mib.mind_polymorphic then
- Univ.UContext.instance mib.mind_universes
+ Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
else Univ.Instance.empty
let inductive_context mib =
if mib.mind_polymorphic then
- Univ.instantiate_univ_context mib.mind_universes
+ Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
else Univ.UContext.empty
(** {6 Hash-consing of inductive declarations } *)
@@ -306,7 +305,7 @@ let hcons_mind mib =
{ mib with
mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
- mind_universes = Univ.hcons_universe_context mib.mind_universes }
+ mind_universes = Univ.hcons_universe_info_ind mib.mind_universes }
(** {6 Stm machinery } *)
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 88584e3b3..97c28025a 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
mind_entry_params : (Id.t * local_entry) list;
mind_entry_inds : one_inductive_entry list;
mind_entry_polymorphic : bool;
- mind_entry_universes : Univ.universe_context * Univ.universe_context;
+ mind_entry_universes : Univ.universe_info_ind;
(* universe constraints and the constraints for subtyping of
inductive types in the block. *)
mind_entry_private : bool option;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5d928facc..94bf1a770 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -220,7 +220,7 @@ let typecheck_inductive env mie =
(* Check unicity of names *)
mind_check_names mie;
(* Params are typed-checked here *)
- let env' = push_context (fst mie.mind_entry_universes) env in
+ let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in
let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
(* We first type arity of each inductive definition *)
(* This allows building the environment of arities and to share *)
@@ -822,10 +822,10 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
let hyps = used_section_variables env inds in
let nparamargs = Context.Rel.nhyps paramsctxt in
let nparamsctxt = Context.Rel.length paramsctxt in
- let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in
- let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in
+ let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in
+ let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in
let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in
- let env_ar =
+ let env_ar =
let ctxunivs = Environ.rel_context env_ar in
let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in
Environ.push_rel_context ctxunivs' env
@@ -842,9 +842,6 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
let consnrealargs =
Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs)
splayed_lc in
- (* Check that the subtyping constraints (inferred outside kernel)
- are valid. If so return (), otherwise raise an anomaly! *)
- let () = () in
(* Elimination sorts *)
let arkind,kelim =
match ar_kind with
@@ -924,8 +921,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
mind_params_ctxt = paramsctxt;
mind_packets = packets;
mind_polymorphic = p;
- mind_universes = ctxunivs;
- mind_subtyping = ctxsbt;
+ mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp);
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f3b03252d..0f0dc0d60 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -55,7 +55,7 @@ let inductive_paramdecls (mib,u) =
let instantiate_inductive_constraints mib u =
if mib.mind_polymorphic then
- Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes)
+ Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes))
else Univ.Constraint.empty
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f5e8e8653..1568fe0bf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -429,7 +429,7 @@ let globalize_mind_universes mb =
if mb.mind_polymorphic then
[Now (true, Univ.ContextSet.empty)]
else
- [Now (false, Univ.ContextSet.of_context mb.mind_universes)]
+ [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))]
let constraints_of_sfb env sfb =
match sfb with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index bdfd00a8d..3cf2299d8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -313,7 +313,7 @@ let infer_declaration ~trust env kn dcl =
in
let term, typ = pb.proj_eta in
Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
- mib.mind_polymorphic, mib.mind_universes, false, None
+ mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None
let global_vars_set_constant_type env = function
| RegularArity t -> global_vars_set env t
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e8b9ae33a..f124bb39e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1053,14 +1053,14 @@ struct
let len = Array.length (Instance.to_array ctx) in
let halflen = len / 2 in
(Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen),
- Instance.of_array (Array.sub (Instance.to_array ctx) halflen len))
+ Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen))
let pr prl (univcst, subtypcst) =
if UContext.is_empty univcst then mt() else
let (ctx, ctx') = halve_context (UContext.instance subtypcst) in
- (UContext.pr prl univcst) ++
- h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "}")
- ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
+ (UContext.pr prl univcst) ++ fnl () ++ fnl () ++
+ h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ")
+ ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
let hcons (univcst, subtypcst) =
(UContext.hcons univcst, UContext.hcons subtypcst)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 74d956bef..fa1662270 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
if Environ.polymorphic_ind ind1 env
then
let mib = Environ.lookup_mind mi env in
- let ulen = Univ.UContext.size mib.Declarations.mind_universes in
+ let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
match stk1 , stk2 with
| [], [] -> assert (Int.equal ulen 0); cu
| Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
diff --git a/library/declare.ml b/library/declare.ml
index 06eeeeab5..f3150174c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -352,7 +352,7 @@ let dummy_inductive_entry (_,m) = ([],{
mind_entry_finite = Decl_kinds.BiFinite;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
mind_entry_polymorphic = false;
- mind_entry_universes = (Univ.UContext.empty, Univ.UContext.empty);
+ mind_entry_universes = Univ.UInfoInd.empty;
mind_entry_private = None;
})
diff --git a/library/global.ml b/library/global.ml
index 1ba86699d..a45998384 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -178,13 +178,13 @@ let type_of_global_unsafe r =
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
let inst =
if mib.Declarations.mind_polymorphic then
- Univ.UContext.instance mib.Declarations.mind_universes
+ Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes)
else Univ.Instance.empty
in
Inductive.type_of_inductive env (specif, inst)
| ConstructRef cstr ->
let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- let inst = Univ.UContext.instance mib.Declarations.mind_universes in
+ let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
Inductive.type_of_constructor (cstr,inst) specif
let type_of_global_in_context env r =
@@ -200,13 +200,13 @@ let type_of_global_in_context env r =
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
let univs =
- if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes
+ if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
else Univ.UContext.empty
in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
| ConstructRef cstr ->
let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
let univs =
- if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes
+ if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
else Univ.UContext.empty
in
let inst = Univ.UContext.instance univs in
@@ -222,10 +222,10 @@ let universes_of_global env r =
(Environ.opaque_tables env) cb
| IndRef ind ->
let (mib, oib) = Inductive.lookup_mind_specif env ind in
- Univ.instantiate_univ_context mib.mind_universes
+ Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
| ConstructRef cstr ->
let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Univ.instantiate_univ_context mib.mind_universes
+ Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
let universes_of_global gr =
universes_of_global (env ()) gr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d7b484281..152ccb079 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -123,7 +123,7 @@ let typeclass_univ_instance (cl,u') =
else Univ.Instance.empty
| IndRef c ->
let mib,oib = Global.lookup_inductive c in
- if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes
+ if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
else Univ.Instance.empty
| _ -> Univ.Instance.empty
in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b08666483..074b7373c 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,7 +174,7 @@ and nf_whd env sigma whd typ =
| Vatom_stk(Aind ((mi,i) as ind), stk) ->
let mib = Environ.lookup_mind mi env in
let nb_univs =
- if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes
+ if mib.mind_polymorphic then Univ.UContext.size (Univ.UInfoInd.univ_context mib.mind_universes)
else 0
in
let mk u =
diff --git a/printing/printer.ml b/printing/printer.ml
index d6f0778f7..c27a9b009 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -261,6 +261,13 @@ let pr_universe_ctx sigma c =
else
mt()
+let pr_universe_info_ind sigma uii =
+ if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then
+ fnl()++pr_in_comment (fun uii -> v 0
+ (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii
+ else
+ mt()
+
(**********************************************************************)
(* Global references *)
diff --git a/printing/printer.mli b/printing/printer.mli
index 3fce06561..6531036a1 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -97,6 +97,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds
val pr_polymorphic : bool -> std_ppcmds
val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds
val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_universe_info_ind : evar_map -> Univ.universe_info_ind -> std_ppcmds
(** Printing global references using names as short as possible *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index c4affd4ac..7dc47a4a4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -89,7 +89,7 @@ let build_ind_type env mip =
let print_one_inductive env sigma mib ((_,i) as ind) =
let u = if mib.mind_polymorphic then
- Univ.UContext.instance mib.mind_universes
+ Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
@@ -100,7 +100,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
let envpar = push_rel_context params env in
let inst =
if mib.mind_polymorphic then
- Printer.pr_universe_instance sigma mib.mind_universes
+ Printer.pr_universe_instance sigma (Univ.UInfoInd.univ_context mib.mind_universes)
else mt ()
in
hov 0 (
@@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib =
def keyword ++ spc () ++
prlist_with_sep (fun () -> fnl () ++ str" with ")
(print_one_inductive env sigma mib) inds ++
- Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
+ Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes))
let get_fields =
let rec prodec_rec l subst c =
@@ -142,7 +142,7 @@ let get_fields =
let print_record env mind mib =
let u =
if mib.mind_polymorphic then
- Univ.UContext.instance mib.mind_universes
+ Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
else Univ.Instance.empty
in
let mip = mib.mind_packets.(0) in
@@ -175,7 +175,7 @@ let print_record env mind mib =
(fun (id,b,c) ->
pr_id id ++ str (if b then " : " else " := ") ++
Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
- Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
+ Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes))
let pr_mutual_inductive_body env mind mib =
if mib.mind_record <> None && not !Flags.raw_print then
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 ? *) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 17:44:36 +0000