aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml2
-rw-r--r--kernel/cClosure.mli6
-rw-r--r--kernel/constr.mli22
-rw-r--r--kernel/declarations.ml6
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/entries.ml10
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/evar.ml1
-rw-r--r--kernel/evar.mli3
-rw-r--r--kernel/indtypes.ml9
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/mod_typing.ml26
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/term.mli20
-rw-r--r--kernel/term_typing.ml46
-rw-r--r--kernel/term_typing.mli2
-rw-r--r--kernel/typeops.mli2
-rw-r--r--kernel/univ.ml1
-rw-r--r--kernel/univ.mli5
-rw-r--r--kernel/vconv.ml2
21 files changed, 101 insertions, 84 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index fa12e54068..31ded9129a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -234,7 +234,7 @@ let unfold_red kn =
* instantiations (cbv or lazy) are.
*)
-type table_key = Constant.t puniverses tableKey
+type table_key = Constant.t Univ.puniverses tableKey
let eq_pconstant_key (c,u) (c',u') =
eq_constant_key c c' && Univ.Instance.equal u u'
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 28136e1fc0..119b70e301 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -92,7 +92,7 @@ val unfold_side_red : reds
val unfold_red : evaluable_global_reference -> reds
(***********************************************************************)
-type table_key = Constant.t puniverses tableKey
+type table_key = Constant.t Univ.puniverses tableKey
type 'a infos_cache
type 'a infos = {
@@ -122,8 +122,8 @@ type fterm =
| FAtom of constr (** Metas and Sorts *)
| FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
- | FInd of inductive puniverses
- | FConstruct of constructor puniverses
+ | FInd of inductive Univ.puniverses
+ | FConstruct of constructor Univ.puniverses
| FApp of fconstr * fconstr array
| FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 4c5ea9e95c..21c477578c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -13,20 +13,22 @@ open Names
(** {6 Value under universe substitution } *)
type 'a puniverses = 'a Univ.puniverses
+[@@ocaml.deprecated "use Univ.puniverses"]
(** {6 Simply type aliases } *)
-type pconstant = Constant.t puniverses
-type pinductive = inductive puniverses
-type pconstructor = constructor puniverses
+type pconstant = Constant.t Univ.puniverses
+type pinductive = inductive Univ.puniverses
+type pconstructor = constructor Univ.puniverses
(** {6 Existential variables } *)
type existential_key = Evar.t
+[@@ocaml.deprecated "use Evar.t"]
(** {6 Existential variables } *)
type metavariable = int
(** {6 Case annotation } *)
-type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
| RegularStyle (** infer printing form from number of constructor *)
type case_printing =
{ ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
@@ -80,7 +82,7 @@ val mkVar : Id.t -> constr
val mkMeta : metavariable -> constr
(** Constructs an existential variable *)
-type existential = existential_key * constr array
+type existential = Evar.t * constr array
val mkEvar : existential -> constr
(** Construct a sort *)
@@ -111,7 +113,7 @@ val mkLetIn : Name.t * constr * types * constr -> constr
{%latex:$(f~t_1\dots f_n)$%}. *)
val mkApp : constr * constr array -> constr
-val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
+val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses
(** Constructs a Constant.t *)
val mkConst : Constant.t -> constr
@@ -180,7 +182,7 @@ val mkCoFix : cofixpoint -> constr
(** [constr array] is an instance matching definitional [named_context] in
the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
+type 'constr pexistential = Evar.t * 'constr array
type ('constr, 'types) prec_declaration =
Name.t array * 'types array * 'constr array
type ('constr, 'types) pfixpoint =
@@ -295,16 +297,16 @@ val decompose_app : constr -> constr * constr list
val decompose_appvect : constr -> constr * constr array
(** Destructs a constant *)
-val destConst : constr -> Constant.t puniverses
+val destConst : constr -> Constant.t Univ.puniverses
(** Destructs an existential variable *)
val destEvar : constr -> existential
(** Destructs a (co)inductive type *)
-val destInd : constr -> inductive puniverses
+val destInd : constr -> inductive Univ.puniverses
(** Destructs a constructor *)
-val destConstruct : constr -> constructor puniverses
+val destConstruct : constr -> constructor Univ.puniverses
(** Destructs a [match c as x in I args return P with ... |
Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b95796fd8f..d5312c5006 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -63,7 +63,7 @@ type constant_def =
| OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *)
type constant_universes =
- | Monomorphic_const of Univ.UContext.t
+ | Monomorphic_const of Univ.ContextSet.t
| Polymorphic_const of Univ.AUContext.t
(** The [typing_flags] are instructions to the type-checker which
@@ -168,9 +168,9 @@ type one_inductive_body = {
}
type abstract_inductive_universes =
- | Monomorphic_ind of Univ.UContext.t
+ | Monomorphic_ind of Univ.ContextSet.t
| Polymorphic_ind of Univ.AUContext.t
- | Cumulative_ind of Univ.ACumulativityInfo.t
+ | Cumulative_ind of Univ.ACumulativityInfo.t
type mutual_inductive_body = {
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f5c26b33d6..d8768a0fc5 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -126,7 +126,7 @@ let hcons_const_def = function
let hcons_const_universes cbu =
match cbu with
| Monomorphic_const ctx ->
- Monomorphic_const (Univ.hcons_universe_context ctx)
+ Monomorphic_const (Univ.hcons_universe_context_set ctx)
| Polymorphic_const ctx ->
Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
@@ -274,7 +274,7 @@ let hcons_mind_packet oib =
let hcons_mind_universes miu =
match miu with
- | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx)
+ | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx)
| Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx)
| Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 185dba409a..c44a17df2a 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -35,9 +35,9 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
*)
type inductive_universes =
- | Monomorphic_ind_entry of Univ.UContext.t
+ | Monomorphic_ind_entry of Univ.ContextSet.t
| Polymorphic_ind_entry of Univ.UContext.t
- | Cumulative_ind_entry of Univ.CumulativityInfo.t
+ | Cumulative_ind_entry of Univ.CumulativityInfo.t
type one_inductive_entry = {
mind_entry_typename : Id.t;
@@ -65,9 +65,11 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
type constant_universes_entry =
- | Monomorphic_const_entry of Univ.UContext.t
+ | Monomorphic_const_entry of Univ.ContextSet.t
| Polymorphic_const_entry of Univ.UContext.t
+type 'a in_constant_universes_entry = 'a * constant_universes_entry
+
type 'a definition_entry = {
const_entry_body : 'a const_entry_body;
(* List of section variables *)
@@ -82,7 +84,7 @@ type 'a definition_entry = {
type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
- Context.Named.t option * bool * types Univ.in_universe_context * inline
+ Context.Named.t option * types in_constant_universes_entry * inline
type projection_entry = {
proj_entry_ind : MutInd.t;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f2066b0659..652ed0f9f7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -7,8 +7,8 @@
(************************************************************************)
open Names
-open Univ
open Constr
+open Univ
open Declarations
(** Unsafe environments. We define here a datatype for environments.
diff --git a/kernel/evar.ml b/kernel/evar.ml
index e63665f519..dcd2e12a0c 100644
--- a/kernel/evar.ml
+++ b/kernel/evar.ml
@@ -13,6 +13,7 @@ let unsafe_of_int x = x
let compare = Int.compare
let equal = Int.equal
let hash = Int.hash
+let print x = Pp.(str "?X" ++ int x)
module Set = Int.Set
module Map = Int.Map
diff --git a/kernel/evar.mli b/kernel/evar.mli
index eee6680fb8..6a058207f6 100644
--- a/kernel/evar.mli
+++ b/kernel/evar.mli
@@ -30,5 +30,8 @@ val compare : t -> t -> int
val hash : t -> int
(** Hash over existential variables. *)
+val print : t -> Pp.t
+(** Printing representation *)
+
module Set : Set.S with type elt = t
module Map : CMap.ExtS with type key = t and module Set := Set
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 083b0ae40f..8e9b606a58 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -265,13 +265,12 @@ let typecheck_inductive env mie =
(* Check unicity of names *)
mind_check_names mie;
(* Params are typed-checked here *)
- let univctx =
+ let env' =
match mie.mind_entry_universes with
- | Monomorphic_ind_entry ctx -> ctx
- | Polymorphic_ind_entry ctx -> ctx
- | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi
+ | 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
in
- let env' = push_context univctx 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 *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 601422a104..a19f87b05b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -7,8 +7,8 @@
(************************************************************************)
open Names
-open Univ
open Constr
+open Univ
open Declarations
open Environ
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 8568bf14b8..f7e755f005 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -79,18 +79,20 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
environment, because they do not appear in the type of the
definition. Any inconsistency will be raised at a later stage
when joining the environment. *)
- let env' = Environ.push_context ~strict:true ctx env' in
- let c',cst = match cb.const_body with
- | Undef _ | OpaqueDef _ ->
- let j = Typeops.infer env' c in
- let typ = cb.const_type in
- let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
- j.uj_type typ in
- j.uj_val, cst'
- | Def cs ->
- let c' = Mod_subst.force_constr cs in
- c, Reduction.infer_conv env' (Environ.universes env') c c'
- in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+ let env' = Environ.push_context ~strict:true ctx env' in
+ let c',cst = match cb.const_body with
+ | Undef _ | OpaqueDef _ ->
+ let j = Typeops.infer env' c in
+ let typ = cb.const_type in
+ let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+ j.uj_type typ in
+ j.uj_val, cst'
+ | Def cs ->
+ let c' = Mod_subst.force_constr cs in
+ c, Reduction.infer_conv env' (Environ.universes env') c c'
+ in
+ let ctx = Univ.ContextSet.of_context ctx in
+ c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
| Polymorphic_const uctx ->
let subst, ctx = Univ.abstract_universes ctx in
let c = Vars.subst_univs_level_constr subst c in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0e416b3e53..0e41bfc3c4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -249,14 +249,14 @@ let universes_of_private eff =
in
match cb.const_universes with
| Monomorphic_const ctx ->
- (Univ.ContextSet.of_context ctx) :: acc
+ ctx :: acc
| Polymorphic_const _ -> acc
)
acc l
| Entries.SEsubproof (c, cb, e) ->
match cb.const_universes with
| Monomorphic_const ctx ->
- (Univ.ContextSet.of_context ctx) :: acc
+ ctx :: acc
| Polymorphic_const _ -> acc
)
[] (Term_typing.uniq_seff eff)
@@ -389,7 +389,6 @@ let push_named_def (id,de) senv =
| Monomorphic_const_entry _ -> false
| Polymorphic_const_entry _ -> true
in
- let univs = Univ.ContextSet.of_context univs in
let c, univs = match c with
| Def c -> Mod_subst.force_constr c, univs
| OpaqueDef o ->
@@ -425,9 +424,8 @@ let labels_of_mib mib =
let globalize_constant_universes env cb =
match cb.const_universes with
- | Monomorphic_const ctx ->
- let cstrs = Univ.ContextSet.of_context ctx in
- Now (false, cstrs) ::
+ | Monomorphic_const cstrs ->
+ Now (false, cstrs) ::
(match cb.const_body with
| (Undef _ | Def _) -> []
| OpaqueDef lc ->
@@ -443,7 +441,7 @@ let globalize_constant_universes env cb =
let globalize_mind_universes mb =
match mb.mind_universes with
| Monomorphic_ind ctx ->
- [Now (false, Univ.ContextSet.of_context ctx)]
+ [Now (false, ctx)]
| Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
| Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
diff --git a/kernel/term.ml b/kernel/term.ml
index 4217cfac79..aa88059524 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -31,7 +31,7 @@ type constr = Constr.t
type types = Constr.t
(** Same as [constr], for documentation purposes. *)
-type existential_key = Constr.existential_key
+type existential_key = Evar.t
type existential = Constr.existential
type metavariable = Constr.metavariable
diff --git a/kernel/term.mli b/kernel/term.mli
index 4efb582d06..f5cb72f4e8 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -129,7 +129,7 @@ val decompose_appvect : constr -> constr * constr array
[@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"]
(** Destructs a constant *)
-val destConst : constr -> Constant.t puniverses
+val destConst : constr -> Constant.t Univ.puniverses
[@@ocaml.deprecated "Alias for [Constr.destConst]"]
(** Destructs an existential variable *)
@@ -137,11 +137,11 @@ val destEvar : constr -> existential
[@@ocaml.deprecated "Alias for [Constr.destEvar]"]
(** Destructs a (co)inductive type *)
-val destInd : constr -> inductive puniverses
+val destInd : constr -> inductive Univ.puniverses
[@@ocaml.deprecated "Alias for [Constr.destInd]"]
(** Destructs a constructor *)
-val destConstruct : constr -> constructor puniverses
+val destConstruct : constr -> constructor Univ.puniverses
[@@ocaml.deprecated "Alias for [Constr.destConstruct]"]
(** Destructs a [match c as x in I args return P with ... |
@@ -407,11 +407,11 @@ val mkInd : inductive -> constr
[@@ocaml.deprecated "Alias for Constr"]
val mkConstruct : constructor -> constr
[@@ocaml.deprecated "Alias for Constr"]
-val mkConstU : Constant.t puniverses -> constr
+val mkConstU : Constant.t Univ.puniverses -> constr
[@@ocaml.deprecated "Alias for Constr"]
-val mkIndU : inductive puniverses -> constr
+val mkIndU : inductive Univ.puniverses -> constr
[@@ocaml.deprecated "Alias for Constr"]
-val mkConstructU : constructor puniverses -> constr
+val mkConstructU : constructor Univ.puniverses -> constr
[@@ocaml.deprecated "Alias for Constr"]
val mkConstructUi : (pinductive * int) -> constr
[@@ocaml.deprecated "Alias for Constr"]
@@ -461,7 +461,7 @@ val map_constr_with_binders :
('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
[@@ocaml.deprecated "Alias for [Constr.map_with_binders]"]
-val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
+val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses
[@@ocaml.deprecated "Alias for [Constr.map_puniverses]"]
val univ_of_sort : Sorts.t -> Univ.Universe.t
[@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"]
@@ -497,7 +497,7 @@ type sorts = Sorts.t =
type sorts_family = Sorts.family = InProp | InSet | InType
[@@ocaml.deprecated "Alias for Sorts.family"]
-type 'a puniverses = 'a Constr.puniverses
+type 'a puniverses = 'a Univ.puniverses
[@@ocaml.deprecated "Alias for Constr.puniverses"]
(** Simply type aliases *)
@@ -507,8 +507,8 @@ type pinductive = Constr.pinductive
[@@ocaml.deprecated "Alias for Constr.pinductive"]
type pconstructor = Constr.pconstructor
[@@ocaml.deprecated "Alias for Constr.pconstructor"]
-type existential_key = Constr.existential_key
-[@@ocaml.deprecated "Alias for Constr.existential_key"]
+type existential_key = Evar.t
+[@@ocaml.deprecated "Alias for Evar.t"]
type existential = Constr.existential
[@@ocaml.deprecated "Alias for Constr.existential"]
type metavariable = Constr.metavariable
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 4617f2d5fa..70dd6438d4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -125,11 +125,10 @@ let inline_side_effects env body ctx side_eff =
| _ -> assert false
in
match cb.const_universes with
- | Monomorphic_const cnstctx ->
+ | Monomorphic_const univs ->
(** Abstract over the term at the top of the proof *)
let ty = cb.const_type in
let subst = Cmap_env.add c (Inr var) subst in
- let univs = Univ.ContextSet.of_context cnstctx in
let ctx = Univ.ContextSet.union ctx univs in
(subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
| Polymorphic_const auctx ->
@@ -228,19 +227,25 @@ let feedback_completion_typecheck =
Option.iter (fun state_id ->
feedback ~id:state_id Feedback.Complete)
-let abstract_constant_universes abstract uctx =
- if not abstract then
+let abstract_constant_universes abstract = function
+ | Monomorphic_const_entry uctx ->
Univ.empty_level_subst, Monomorphic_const uctx
- else
- let sbst, auctx = Univ.abstract_universes uctx in
- sbst, Polymorphic_const auctx
+ | Polymorphic_const_entry uctx ->
+ if not abstract then
+ Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx)
+ else
+ let sbst, auctx = Univ.abstract_universes uctx in
+ sbst, Polymorphic_const auctx
let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
match dcl with
- | ParameterEntry (ctx,poly,(t,uctx),nl) ->
- let env = push_context ~strict:(not poly) uctx env in
+ | 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
+ in
let j = infer env t in
- let abstract = poly && not (Option.is_empty kn) in
+ let abstract = not (Option.is_empty kn) in
let usubst, univs =
abstract_constant_universes abstract uctx
in
@@ -262,7 +267,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
const_entry_universes = Monomorphic_const_entry univs } as c) ->
- let env = push_context ~strict:true univs env in
+ let env = push_context_set ~strict:true univs env in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let tyj = infer_type env typ in
let proofterm =
@@ -301,21 +306,22 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let (body, ctx), side_eff = Future.join body in
- let poly, univs = match c.const_entry_universes with
+ let poly, univsctx = match c.const_entry_universes with
| Monomorphic_const_entry univs -> false, univs
- | Polymorphic_const_entry univs -> true, univs
+ | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs
in
- let univsctx = Univ.ContextSet.of_context univs in
let ctx = Univ.ContextSet.union univsctx ctx in
let body, ctx, _ = match trust with
| Pure -> body, ctx, []
| SideEffects _ -> inline_side_effects env body ctx side_eff
in
let env = push_context_set ~strict:(not poly) ctx env in
- let abstract = poly && not (Option.is_empty kn) in
- let usubst, univs =
- abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
- in
+ let abstract = not (Option.is_empty kn) in
+ let ctx = if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
+ else Monomorphic_const_entry ctx
+ in
+ let usubst, univs = abstract_constant_universes abstract ctx in
let j = infer env body in
let typ = match typ with
| None ->
@@ -556,7 +562,7 @@ let export_side_effects mb env ce =
let env = Environ.add_constant kn cb env in
match cb.const_universes with
| Monomorphic_const ctx ->
- Environ.push_context ~strict:true ctx env
+ Environ.push_context_set ~strict:true ctx env
| Polymorphic_const _ -> env
end
| kn, cb, `Opaque(_, ctx), _ ->
@@ -564,7 +570,7 @@ let export_side_effects mb env ce =
let env = Environ.add_constant kn cb env in
match cb.const_universes with
| Monomorphic_const cstctx ->
- let env = Environ.push_context ~strict:true cstctx env in
+ let env = Environ.push_context_set ~strict:true cstctx env in
Environ.push_context_set ~strict:true ctx env
| Polymorphic_const _ -> env
end
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 9b35bfc6e8..55da4197e2 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -19,7 +19,7 @@ type _ trust =
| SideEffects : structure_body -> side_effects trust
val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
- constant_def * types * Univ.UContext.t
+ constant_def * types * Univ.ContextSet.t
val translate_local_assum : env -> types -> types
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 3aaad5877b..5584b6ab46 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -7,8 +7,8 @@
(************************************************************************)
open Names
-open Univ
open Constr
+open Univ
open Environ
open Entries
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7fe4f82748..64afb95d56 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1053,6 +1053,7 @@ struct
let constraints (univs, cst) = cst
let levels (univs, cst) = univs
+ let size (univs,_) = LSet.cardinal univs
end
type universe_context_set = ContextSet.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 8d46a8beef..c06ce2446f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -310,7 +310,7 @@ sig
(** Keeps the order of the instances *)
val union : t -> t -> t
- (* the number of universes in the context *)
+ (** the number of universes in the context *)
val size : t -> int
end
@@ -423,6 +423,9 @@ sig
val constraints : t -> constraints
val levels : t -> LSet.t
+
+ (** the number of universes in the context *)
+ val size : t -> int
end
(** A set of universes with universe constraints.
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 0e452621c8..578a893718 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
let mib = Environ.lookup_mind mi env in
let ulen =
match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx
+ | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx
| Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
| Declarations.Cumulative_ind cumi ->
Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:10:56 +0000