Merge branch 'v8.5'

1 files changed, 4 insertions, 2 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 4cc34e41e..fab0e6fb8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,7 +937,9 @@ struct
     else if Array.length y = 0 then x 
     else Array.append x y
 
-  let of_array a = a
+  let of_array a =
+    assert(Array.for_all (fun x -> not (Level.is_prop x)) a);
+    a
 
   let to_array a = a
 
@@ -945,7 +947,7 @@ struct
 
   let subst_fn fn t = 
     let t' = CArray.smartmap fn t in
-      if t' == t then t else t'
+      if t' == t then t else of_array t'
 
   let levels x = LSet.of_array x