From c9f3a6cbe5c410256fe88580019f5c7183bab097 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Wed, 7 Feb 2018 18:58:16 +0100
Subject: Fix #6677: Critical bug with VM and universes

This bug was present since the first patch adding universe polymorphism
handling in the VM (Coq 8.5). Note that unsoundness can probably be
observed even without universe polymorphism.
---
 kernel/univ.mli | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'kernel/univ.mli')

diff --git a/kernel/univ.mli b/kernel/univ.mli
index 63bef1b81..f550872ba 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
-- 
cgit v1.2.3