Merge PR #6713: Fix #6677: Critical bug with VM and universes

1 files changed, 7 insertions, 0 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index 77ebf5a11..c45ebe21c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -125,6 +125,13 @@ sig
   val for_all : (Level.t * int -> bool) -> t -> bool
 
   val map : (Level.t * int -> 'a) -> t -> 'a list
+
+  (** [compact u] remaps local variables in [u] such that their indices become
+       consecutive. It returns the new universe and the mapping.
+       Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] =
+         [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
+  *)
+  val compact : t -> t * int list
 end
 
 type universe = Universe.t