diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/environ.mli | 6 | ||||
| -rw-r--r-- | kernel/indTyping.ml | 2 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 6 | ||||
| -rw-r--r-- | kernel/uGraph.mli | 10 |
5 files changed, 20 insertions, 8 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index d6d52dbc2b..182ed55d0e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -67,7 +67,7 @@ end type stratification = { env_universes : UGraph.t; env_sprop_allowed : bool; - env_universes_lbound : Univ.Level.t; + env_universes_lbound : UGraph.Bound.t; env_engagement : engagement } @@ -129,7 +129,7 @@ let empty_env = { env_stratification = { env_universes = UGraph.initial_universes; env_sprop_allowed = true; - env_universes_lbound = Univ.Level.set; + env_universes_lbound = UGraph.Bound.Set; env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; diff --git a/kernel/environ.mli b/kernel/environ.mli index 7a46538772..79e632daa0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -62,7 +62,7 @@ end type stratification = { env_universes : UGraph.t; env_sprop_allowed : bool; - env_universes_lbound : Univ.Level.t; + env_universes_lbound : UGraph.Bound.t; env_engagement : engagement } @@ -96,8 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t -val universes_lbound : env -> Univ.Level.t -val set_universes_lbound : env -> Univ.Level.t -> env +val universes_lbound : env -> UGraph.Bound.t +val set_universes_lbound : env -> UGraph.Bound.t -> env val rel_context : env -> Constr.rel_context val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 8ac96a6481..e9687991c0 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -321,7 +321,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = if has_template_poly then (* For that particular case, we typecheck the inductive in an environment where the universes introduced by the definition are only [>= Prop] *) - let env = set_universes_lbound env Univ.Level.prop in + let env = set_universes_lbound env UGraph.Bound.Prop in push_context_set ~strict:false ctx env else (* In the regular case, all universes are [> Set] *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 5f5f0ef8cd..927db9e9e6 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -148,8 +148,14 @@ let enforce_leq_alg u v g = assert (check_leq g u v); cg +module Bound = +struct + type t = Prop | Set +end + exception AlreadyDeclared = G.AlreadyDeclared let add_universe u ~lbound ~strict g = + let lbound = match lbound with Bound.Prop -> Level.prop | Bound.Set -> Level.set in let graph = G.add u g.graph in let d = if strict then Lt else Le in enforce_constraint (lbound,d,u) {g with graph} diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 8d9afb0990..c9fbd7f694 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -48,7 +48,13 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t exception AlreadyDeclared -val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t +module Bound : +sig + type t = Prop | Set + (** The [Prop] bound is only used for template polymorphic inductive types. *) +end + +val add_universe : Level.t -> lbound:Bound.t -> strict:bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t @@ -86,7 +92,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t val domain : t -> LSet.t (** Known universes *) -val check_subtype : lbound:Level.t -> AUContext.t check_function +val check_subtype : lbound:Bound.t -> AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) |