diff options
Diffstat (limited to 'kernel/univ.ml')
-rw-r--r-- | kernel/univ.ml | 6 |
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 |