From b8f1b16cfeebcb6dbcd24a3f955598e31a0cb04b Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 10 Jan 2017 06:44:42 +0100
Subject: [PATCH] chore(init/meta/smt/congruence_closure): remove unnecessary
 line

---
 library/init/meta/smt/congruence_closure.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/library/init/meta/smt/congruence_closure.lean b/library/init/meta/smt/congruence_closure.lean
index b4fd85c17f..6282452091 100644
--- a/library/init/meta/smt/congruence_closure.lean
+++ b/library/init/meta/smt/congruence_closure.lean
@@ -121,7 +121,6 @@ do (lhs, rhs) ← target >>= match_eq,
    s ← s^.internalize rhs,
    b ← s^.is_eqv lhs rhs,
    if b then do {
-     t ← return $ expr.const `true [],
      s^.eqv_proof lhs rhs >>= exact
    } else do {
      fail "ac_refl failed"