From 1d301b781346901cd0c099a77cb5edf2b7333bcc Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 14 Feb 2017 21:02:35 +0100
Subject: [PATCH] feat(init/meta/smt/congruence_closure): add
 has_to_tactic_format instance

---
 library/init/meta/smt/congruence_closure.lean | 6 +++---
 tests/lean/run/cc1.lean                       | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/init/meta/smt/congruence_closure.lean b/library/init/meta/smt/congruence_closure.lean
index 5a5a63f6e5..445b07fae3 100644
--- a/library/init/meta/smt/congruence_closure.lean
+++ b/library/init/meta/smt/congruence_closure.lean
@@ -56,8 +56,8 @@ cc_state.mk_using_hs_core {}
 meta def roots (s : cc_state) : list expr :=
 cc_state.roots_core s tt
 
-meta def pp (s : cc_state) : tactic format :=
-cc_state.pp_core s tt
+meta instance : has_to_tactic_format cc_state :=
+⟨λ s, cc_state.pp_core s tt⟩
 
 meta def eqc_of_core (s : cc_state) : expr → expr → list expr → list expr
 | e f r :=
@@ -100,7 +100,7 @@ do intros, s ← cc_state.mk_using_hs_core cfg, t ← target, s ← s^.internali
      } else do {
        dbg ← get_bool_option `trace.cc.failure ff,
        if dbg then do {
-         ccf ← s^.pp,
+         ccf ← pp s,
          msg ← return $ to_fmt "cc tactic failed, equivalence classes: " ++ format.line ++ ccf,
          fail msg
        } else do {
diff --git a/tests/lean/run/cc1.lean b/tests/lean/run/cc1.lean
index d0a1af4220..2df4edfd87 100644
--- a/tests/lean/run/cc1.lean
+++ b/tests/lean/run/cc1.lean
@@ -5,7 +5,7 @@ set_option pp.implicit true
 example (a b c d : nat) (f : nat → nat → nat) : a = b → b = c → d + (if b > 0 then a else b) = 0 → f (b + b) b ≠ f (a + c) c → false :=
 by do intros,
       s ← cc_state.mk_using_hs,
-      s^.pp >>= trace,
+      trace s,
       t₁ ← to_expr `(f (b + b) b),
       t₂ ← to_expr `(f (a + c) c),
       b  ← to_expr `(b),