Fix #6956: Uncaught exception in bytecode compilation

We also make the code of [compact] in kernel/univ.ml a bit clearer.

1 files changed, 7 insertions, 6 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index 629d83fb8..aaed899bf 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -128,12 +128,6 @@ sig
 
   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
@@ -504,6 +498,13 @@ val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativit
 
 val make_abstract_instance : AUContext.t -> Instance.t
 
+(** [compact_univ u] remaps local variables in [u] such that their indices become
+     consecutive. It returns the new universe and the mapping.
+     Example: compact_univ [(Var 0, i); (Prop, 0); (Var 2; j))] =
+       [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
+*)
+val compact_univ : Universe.t -> Universe.t * int list
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.t