diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-03 23:45:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-03 23:45:01 +0200 |
| commit | 23d30ddc2a7cdfa3f71e99f57d36818b16ad40b7 (patch) | |
| tree | bdd895f74d2764e4e57a1c4aab65ba4408442190 /kernel/univ.mli | |
| parent | 7e4925b78162226331c65ef77f2da681a0b8ee48 (diff) | |
Cleanup code related to the constraint solving, which sits now outside the
kernel in library/universes.ml.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 27 |
1 files changed, 9 insertions, 18 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 8166d75e6..9b68dbc8c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -129,6 +129,15 @@ val super : universe -> universe val universe_level : universe -> universe_level option +(** [univ_level_mem l u] Is l is mentionned in u ? *) + +val univ_level_mem : universe_level -> universe -> bool + +(** [univ_level_rem u v min] removes [u] from [v], resulting in [min] + if [v] was exactly [u]. *) + +val univ_level_rem : universe_level -> universe -> universe -> universe + (** {6 Graphs of universes. } *) type universes @@ -211,24 +220,6 @@ val constraints_of_universes : universes -> constraints val check_constraint : universes -> univ_constraint -> bool val check_constraints : constraints -> universes -> bool -(** {6 Support for old-style sort-polymorphism } *) - -val solve_constraints_system : universe option array -> universe array -> universe array -> - universe array - -val remove_large_constraint : universe_level -> universe -> universe -> universe - -val subst_large_constraint : universe -> universe -> universe -> universe - -val subst_large_constraints : - (universe * universe) list -> universe -> universe - -val no_upper_constraints : universe -> constraints -> bool - -(** Is u mentionned in v (or equals to v) ? *) - -val univ_depends : universe -> universe -> bool - (** {6 Support for universe polymorphism } *) (** Polymorphic maps from universe levels to 'a *) |