From ada260309e2d30b2ecb153ddba1c10b4b4aa8bb3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Jul 2016 17:07:09 -0700
Subject: [PATCH] refactor(library/init/meta): move defeq simplifier related
 tactics to separate file

---
 library/init/meta/default.lean           |  2 +-
 library/init/meta/defeq_simp_tactic.lean | 27 ++++++++++++++++++++++++
 library/init/meta/tactic.lean            | 19 -----------------
 3 files changed, 28 insertions(+), 20 deletions(-)
 create mode 100644 library/init/meta/defeq_simp_tactic.lean

diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean
index 5a0d52de34..37362d3ba5 100644
--- a/library/init/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -11,4 +11,4 @@ import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info
 import init.meta.congr_lemma init.meta.match_tactic init.meta.ac_tactics
 import init.meta.backward init.meta.rewrite_tactic init.meta.unfold_tactic
 import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance
-import init.meta.simp_tactic
+import init.meta.simp_tactic init.meta.defeq_simp_tactic
diff --git a/library/init/meta/defeq_simp_tactic.lean b/library/init/meta/defeq_simp_tactic.lean
new file mode 100644
index 0000000000..24da667a51
--- /dev/null
+++ b/library/init/meta/defeq_simp_tactic.lean
@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic
+
+namespace tactic
+/- Simplify the given expression using [defeq] lemmas.
+   The resulting expression is definitionally equal to the input. -/
+meta_constant defeq_simp_core : transparency → expr → tactic expr
+
+meta_definition defeq_simp : expr → tactic expr :=
+defeq_simp_core reducible
+
+meta_definition dsimp : tactic unit :=
+target >>= defeq_simp >>= change
+
+meta_definition dsimp_at (H : expr) : tactic unit :=
+do num_reverted : ℕ ← revert H,
+   (expr.pi n bi d b : expr) ← target | failed,
+   H_simp : expr ← defeq_simp d,
+   change $ expr.pi n bi H_simp b,
+   intron num_reverted
+
+end tactic
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 8529840598..5a592c2e6b 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -163,9 +163,6 @@ meta_constant to_expr       : qexpr → tactic expr
 meta_constant is_class      : expr → tactic bool
 /- Try to create an instance of the given type class. -/
 meta_constant mk_instance   : expr → tactic expr
-/- Simplify the given expression using [defeq] lemmas.
-   The resulting expression is definitionally equal to the input. -/
-meta_constant defeq_simp_core : transparency → expr → tactic expr
 /- Change the target of the main goal.
    The input expression must be definitionally equal to the current target. -/
 meta_constant change        : expr → tactic unit
@@ -316,22 +313,6 @@ do gs ← get_goals,
    | _              := skip
    end
 
--- TODO(Leo): remove unifier.conservative after we finish new elaborator
-set_option unifier.conservative true
-
-meta_definition defeq_simp : expr → tactic expr :=
-defeq_simp_core reducible
-
-meta_definition dsimp : tactic unit :=
-target >>= defeq_simp >>= change
-
-meta_definition dsimp_at (H : expr) : tactic unit :=
-do num_reverted : ℕ ← revert H,
-   (expr.pi n bi d b : expr) ← target | failed,
-   H_simp : expr ← defeq_simp d,
-   change $ expr.pi n bi H_simp b,
-   intron num_reverted
-
 /- Return the number of goals that need to be solved -/
 meta_definition num_goals     : tactic nat :=
 do gs ← get_goals,