chore(library/meta/tactic): remove duplicate todo

2016-07-03 02:36:50 +01:00 · 2016-07-03 02:36:50 +01:00 · ba756eec4b
commit ba756eec4b
parent 044a61d350
1 changed files with 0 additions and 3 deletions
--- 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,