1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index dc0a4b43c..2b3a2bdb1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1707,7 +1707,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
 
@@ -1715,7 +1717,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