diff options
| author | Guillaume Melquiond | 2015-11-23 08:14:27 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-11-23 08:14:27 +0100 |
| commit | 6b3112d3b6e401a4c177447dd3651820897f711f (patch) | |
| tree | 53509759b6b562abcd28726e2473400ba721d714 /kernel | |
| parent | c4e2cf027b3fade4f9c2806e6061e1294a99e540 (diff) | |
Fix output of universe arcs. (Fix bug #4422)
Diffstat (limited to 'kernel')
| -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 6c2316988e..dc0a4b43c0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -2030,8 +2030,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 |