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

1 files changed, 35 insertions, 2 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 080bb7ad4..fbb047364 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -266,7 +266,7 @@ struct
   module Expr = 
   struct
     type t = Level.t * int
-	
+
     (* Hashing of expressions *)
     module ExprHash = 
     struct
@@ -487,7 +487,40 @@ struct
       | [] -> cons a l
     in 
       List.fold_right (fun a acc -> aux a acc) u []
-	
+
+  (** [max_var_pred p u] returns the maximum variable level in [u] satisfying
+      [p], -1 if not found *)
+  let rec max_var_pred p u =
+    let open Level in
+    match u with
+    | [] -> -1
+    | (v, _) :: u ->
+      match var_index v with
+      | Some i when p i -> max i (max_var_pred p u)
+      | _ -> max_var_pred p u
+
+  let rec remap_var u i j =
+    let open Level in
+    match u with
+    | [] -> []
+    | (v, incr) :: u when var_index v = Some i ->
+      (Level.var j, incr) :: remap_var u i j
+    | _ :: u -> remap_var u i j
+
+  let rec compact u max_var i =
+    if i >= max_var then (u,[]) else
+    let j = max_var_pred (fun j -> j < i) u in
+    if Int.equal i (j+1) then
+      let (u,s) = compact u max_var (i+1) in
+      (u, i :: s)
+    else
+      let (u,s) = compact (remap_var u i j) max_var (i+1) in
+      (u, j+1 :: s)
+
+  let compact u =
+    let max_var = max_var_pred (fun _ -> true) u in
+    compact u max_var 0
+
   (* Returns the formal universe that is greater than the universes u and v.
      Used to type the products. *)
   let sup x y = merge_univs x y