diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 3 | ||||
| -rw-r--r-- | kernel/univ.mli | 3 |
3 files changed, 7 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 7759efb67..7a41e62c4 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -197,7 +197,7 @@ let add_mind kn mib env = (* Universe constraints *) let add_constraints c env = - if c == empty_constraint then + if is_empty_constraint c then env else let s = env.env_stratification in diff --git a/kernel/univ.ml b/kernel/univ.ml index 7f458f64c..a89345440 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -171,6 +171,7 @@ let is_univ_variable = function let type1_univ = Max ([], [UniverseLevel.Set]) let initial_universes = UniverseLMap.empty +let is_initial_universes = UniverseLMap.is_empty (* Every UniverseLevel.t has a unique canonical arc representative *) @@ -485,6 +486,8 @@ module Constraint = Set.Make( type constraints = Constraint.t let empty_constraint = Constraint.empty +let is_empty_constraint = Constraint.is_empty + let union_constraints = Constraint.union type constraint_function = diff --git a/kernel/univ.mli b/kernel/univ.mli index a55775372..8b3f62910 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -47,6 +47,7 @@ val check_eq : check_function (** The empty graph of universes *) val initial_universes : universes +val is_initial_universes : universes -> bool (** {6 Constraints. } *) @@ -55,6 +56,8 @@ type constraints val empty_constraint : constraints val union_constraints : constraints -> constraints -> constraints +val is_empty_constraint : constraints -> bool + type constraint_function = universe -> universe -> constraints -> constraints val enforce_geq : constraint_function |