diff options
| author | Gaëtan Gilbert | 2017-09-09 14:00:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2017-09-19 10:28:03 +0200 |
| commit | cd29948855c2cbd3f4065170e41f8dbe625e1921 (patch) | |
| tree | e747c92a12074f2d0753b902c5fe00261d0a0fe4 /kernel | |
| parent | c2b881aae9c71a34199d2c66282512f2bdb19cf6 (diff) | |
Don't lose names in UState.universe_context.
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index a4f2e26b63..94116e4737 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -411,6 +411,7 @@ sig val add_instance : Instance.t -> t -> t (** Arbitrary choice of linear order of the variables *) + val sort_levels : Level.t array -> Level.t array val to_context : t -> universe_context val of_context : universe_context -> t |