diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 6c231698..21ffafed 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 @@ -2030,8 +2032,8 @@ let dump_universes output g = let dump_arc u = function | Canonical {univ=u; lt=lt; le=le} -> let u_str = Level.to_string u in - List.iter (fun v -> output Lt (Level.to_string v) u_str) lt; - List.iter (fun v -> output Le (Level.to_string v) u_str) le + List.iter (fun v -> output Lt u_str (Level.to_string v)) lt; + List.iter (fun v -> output Le u_str (Level.to_string v)) le | Equiv v -> output Eq (Level.to_string u) (Level.to_string v) in |