From 744a07e53fb99652b2b30520cfe3dfe701bbde18 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Nov 2018 12:45:00 +0100
Subject: 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.
---
 kernel/univ.ml                    | 6 +++---
 test-suite/output/UnivBinders.out | 3 +--
 2 files changed, 4 insertions(+), 5 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
 
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d63b6dbfce..4d3f7419e6 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -41,8 +41,7 @@ Arguments A, Wrap are implicit and maximally inserted
 Argument scopes are [type_scope _]
 Polymorphic bar@{u} = nat
      : Wrap@{u} Set
-(* u |= Set < u
-         *)
+(* u |= Set < u *)
 
 bar is universe polymorphic
 Polymorphic foo@{u UnivBinders.17 v} = 
-- 
cgit v1.2.3