From cd29948855c2cbd3f4065170e41f8dbe625e1921 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 9 Sep 2017 14:00:42 +0200
Subject: 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.
---
 kernel/univ.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel')

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
 
-- 
cgit v1.2.3