diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-11-23 08:14:27 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-11-23 08:14:27 +0100 |
| commit | 6b3112d3b6e401a4c177447dd3651820897f711f (patch) | |
| tree | 53509759b6b562abcd28726e2473400ba721d714 | |
| parent | c4e2cf027b3fade4f9c2806e6061e1294a99e540 (diff) | |
Fix output of universe arcs. (Fix bug #4422)
| -rw-r--r-- | kernel/univ.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 13 |
2 files changed, 7 insertions, 10 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 6c2316988..dc0a4b43c 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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b6a1a53fa..177c3fb0a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -355,11 +355,6 @@ let dump_universes_gen g s = close (); iraise reraise -let dump_universes sorted s = - let g = Global.universes () in - let g = if sorted then Univ.sort_universes g else g in - dump_universes_gen g s - (*********************) (* "Locate" commands *) @@ -1623,15 +1618,17 @@ let vernac_print = function | PrintCoercionPaths (cls,clt) -> msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) - | PrintUniverses (b, None) -> + | PrintUniverses (b, dst) -> let univ = Global.universes () in let univ = if b then Univ.sort_universes univ else univ in let pr_remaining = if Global.is_joined_environment () then mt () else str"There may remain asynchronous universe constraints" in - msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) - | PrintUniverses (b, Some s) -> dump_universes b s + begin match dst with + | None -> msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) + | Some s -> dump_universes_gen univ s + end | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) |