From ba756eec4bddd197497cba0cc439f7e76912d910 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Sun, 3 Jul 2016 02:36:50 +0100
Subject: [PATCH] chore(library/meta/tactic): remove duplicate todo

---
 library/init/meta/tactic.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index eaaa4b5775..735abc8ce0 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -290,9 +290,6 @@ do num_reverted : ℕ ← revert H,
    change $ expr.pi n bi H_simp b,
    intron num_reverted
 
--- TODO(Leo): remove unifier.conservative after we finish new elaborator
-set_option unifier.conservative true
-
 meta_definition simp : tactic unit :=
 do (new_target, Heq) ← target >>= simplify,
    assert "Htarget" new_target, swap,