feat(init/meta/smt/congruence_closure): add has_to_tactic_format instance

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 {

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),