From 6329afc121fc1f30e3df4904d0adbaeb0c8bc590 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Dec 2016 19:13:15 -0800
Subject: [PATCH] chore(library/tactic/congruence/congruence_closure): fix typo

---
 src/library/tactic/congruence/congruence_closure.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp
index 8fd8a254fd..a8bae49783 100644
--- a/src/library/tactic/congruence/congruence_closure.cpp
+++ b/src/library/tactic/congruence/congruence_closure.cpp
@@ -1287,10 +1287,10 @@ format congruence_closure::state::pp_eqcs(formatter const & fmt) const {
     format r;
     bool first = true;
     for (expr const & root : roots) {
-        if (first) first = false; r += line();
+        if (first) first = false; else r += comma() + line();
         r += pp_eqc(fmt, root);
     }
-    return r;
+    return bracket("{", group(r), "}");
 }
 
 void initialize_congruence_closure() {