We improve a little bit in printing universe constraints signature mismatch.

Use of boxes to ensure locality of formatting + use of a
prlist_with_sep so that there are breaking points only inbetween the
elements and not at the end of the list.

1 files changed, 3 insertions, 3 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0edf750997..2b3b4f9486 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -570,9 +570,9 @@ struct
   include S
 
   let pr prl c =
-    fold (fun (u1,op,u2) pp_std ->
-      pp_std ++ prl u1 ++ pr_constraint_type op ++
-	prl u2 ++ fnl () )  c (str "")
+    v 0 (prlist_with_sep spc (fun (u1,op,u2) ->
+      hov 0 (prl u1 ++ pr_constraint_type op ++ prl u2))
+       (elements c))
 
 end