From 646cdfdf40a86c89e437d7aced78c133da93c818 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Aug 2018 15:14:22 -0700
Subject: [PATCH] chore(library/init/meta): remove well_founded_tactics

---
 library/init/default.lean                   |  2 +-
 library/init/meta/well_founded_tactics.lean | 23 ---------------------
 2 files changed, 1 insertion(+), 24 deletions(-)
 delete mode 100644 library/init/meta/well_founded_tactics.lean

diff --git a/library/init/default.lean b/library/init/default.lean
index 69dcbfd8d1..de062e2e9c 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -6,4 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.core init.control init.data.basic init.version
 import init.function init.util init.coe init.wf init.meta
-import init.meta.well_founded_tactics init.data init.io
+import init.data init.io
diff --git a/library/init/meta/well_founded_tactics.lean b/library/init/meta/well_founded_tactics.lean
deleted file mode 100644
index 3bf098eacf..0000000000
--- a/library/init/meta/well_founded_tactics.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2017 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
-
-/-- Argument for using_well_founded
-
-  The tactic `rel_tac` has to synthesize an element of type (has_well_founded A).
-  The two arguments are: a local representing the function being defined by well
-  founded recursion, and a list of recursive equations.
-  The equations can be used to decide which well founded relation should be used.
-
-  The tactic `dec_tac` has to synthesize decreasing proofs.
--/
-meta structure well_founded_tactics :=
-(rel_tac : expr → list expr → tactic unit := λ _ _, tactic.apply_instance)
-(dec_tac : tactic unit := tactic.assumption)
-
-meta def well_founded_tactics.default : well_founded_tactics :=
-{}