diff options
| -rw-r--r-- | kernel/uGraph.ml | 5 | ||||
| -rw-r--r-- | kernel/uGraph.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 11 |
3 files changed, 10 insertions, 8 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index ad94362aaf..9083156745 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -967,12 +967,11 @@ let pr_universes prl g = let dump_universes output g = let dump_arc u = function | Canonical {univ=u; ltle; _} -> - let u_str = Level.to_string u in UMap.iter (fun v strict -> let typ = if strict then Lt else Le in - output typ u_str (Level.to_string v)) ltle; + output typ u v) ltle; | Equiv v -> - output Eq (Level.to_string u) (Level.to_string v) + output Eq u v in UMap.iter dump_arc g.entries diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 4336a22b8c..a2cc5b3116 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -86,7 +86,7 @@ val check_subtype : AUContext.t check_function (** {6 Dumping to a file } *) val dump_universes : - (constraint_type -> string -> string -> unit) -> t -> unit + (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit (** {6 Debugging} *) val check_universes_invariants : t -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bc554fb4bf..7a76fb9560 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -319,7 +319,7 @@ let print_registered () = hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ()) -let dump_universes_gen g s = +let dump_universes_gen prl g s = let output = open_out s in let output_constraint, close = if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin @@ -344,10 +344,12 @@ let dump_universes_gen g s = | Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=" - in Printf.fprintf output "%s %s %s ;\n" left kind right + in + Printf.fprintf output "%s %s %s ;\n" left kind right end, (fun () -> close_out output) end in + let output_constraint k l r = output_constraint k (prl l) (prl r) in try UGraph.dump_universes output_constraint g; close (); @@ -381,9 +383,10 @@ let print_universes ?loc ~sort ~subgraph dst = if Global.is_joined_environment () then mt () else str"There may remain asynchronous universe constraints" in + let prl = UnivNames.pr_with_global_universes in begin match dst with - | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining - | Some s -> dump_universes_gen univ s + | None -> UGraph.pr_universes prl univ ++ pr_remaining + | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s end (*********************) |