diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-08 18:13:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:47 +0100 |
| commit | 921ea3983d45051ae85b0e20bf13de2eff38e53e (patch) | |
| tree | 6b8a7f33e7df5d2eac0c81a8839ca6d749fad752 /checker/reduction.ml | |
| parent | 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 (diff) | |
[pp] Remove uses of expensive string_of_ppcmds.
In general we want to avoid this as much as we can, as it will need to
make choices regarding the output backend (width, etc...) and it is
expensive. It is better to serve the printing backends the pretty
print document itself.
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index ec16aa261..28c0126b4 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -176,9 +176,9 @@ let sort_cmp env univ pb s0 s1 = then begin if !Flags.debug then begin let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds - (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() - ++ Univ.pr_universes univ)) + Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( + str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() + ++ Univ.pr_universes univ) end; raise NotConvertible end |