diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-08-18 19:14:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-08-18 19:15:28 +0200 |
| commit | a398e90fe0828d62a2a2a9ecc87bd3c8d29daf8c (patch) | |
| tree | 2d0b7e08dcc575ae1baab4560d16f8a431a59120 /kernel/univ.ml | |
| parent | efa1c32a4d17870794dbc6f0301c3c0d46637a55 (diff) | |
Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger than Type.1 etc...
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 942c90aa2..fbdb5bb0d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -2088,8 +2088,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 u_str (Level.to_string v)) lt; - List.iter (fun v -> output Le u_str (Level.to_string v)) le + 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 | Equiv v -> output Eq (Level.to_string u) (Level.to_string v) in |