From 215a3ac8fd132fd2154bb98ad78c09bdca500b48 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Aug 2019 08:58:59 -0700
Subject: [PATCH] chore(library/tactic/clear_tactic): remove dead code

---
 src/library/tactic/clear_tactic.cpp | 21 ---------------------
 src/library/tactic/clear_tactic.h   |  3 ---
 2 files changed, 24 deletions(-)

diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp
index 9f3f3143de..6e0ede2e43 100644
--- a/src/library/tactic/clear_tactic.cpp
+++ b/src/library/tactic/clear_tactic.cpp
@@ -27,27 +27,6 @@ expr clear(metavar_context & mctx, expr const & mvar, expr const & H) {
     return new_mvar;
 }
 
-expr clear_rec_core(metavar_context & mctx, expr const & mvar) {
-    optional<metavar_decl> g   = mctx.find_metavar_decl(mvar);
-    lean_assert(g);
-    local_context lctx         = g->get_context();
-    if (optional<local_decl> d = lctx.find_if([](local_decl const & decl) { return is_rec(decl.get_info()); })) {
-        return clear(mctx, mvar, d->mk_ref());
-    } else {
-        return mvar;
-    }
-}
-
-expr clear_recs(metavar_context & mctx, expr const & mvar) {
-    expr curr = mvar;
-    while (true) {
-        expr next = clear_rec_core(mctx, curr);
-        if (next == curr)
-            return curr;
-        curr = next;
-    }
-}
-
 void initialize_clear_tactic() {
 }
 
diff --git a/src/library/tactic/clear_tactic.h b/src/library/tactic/clear_tactic.h
index a9335e1de1..bc68314b4b 100644
--- a/src/library/tactic/clear_tactic.h
+++ b/src/library/tactic/clear_tactic.h
@@ -8,9 +8,6 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic_state.h"
 namespace lean {
 expr clear(metavar_context & mctx, expr const & mvar, expr const & H);
-/* Eliminate hypotheses that are marked as 'rec'
-   (i.e., auxiliary hypotheses generated by the equation compiler). */
-expr clear_recs(metavar_context & mctx, expr const & mvar);
 void initialize_clear_tactic();
 void finalize_clear_tactic();
 }