From fd17a19a231c7af102d26706e096b01ba0dfd9f1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 Jun 2017 15:32:08 -0700
Subject: [PATCH] chore(library/tactic/simplify): remove dead option

---
 src/library/inductive_compiler/nested.cpp | 1 -
 src/library/tactic/simplify.h             | 3 ---
 2 files changed, 4 deletions(-)

diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index a43b5416ed..4e6812944b 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -1554,7 +1554,6 @@ class add_nested_inductive_decl_fn {
         cfg.m_canonize_proofs    = false;
         cfg.m_use_axioms         = false;
         cfg.m_zeta               = false;
-        cfg.m_use_matcher        = false;
         return cfg;
     }
 
diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h
index da65748f84..2b568d87f5 100644
--- a/src/library/tactic/simplify.h
+++ b/src/library/tactic/simplify.h
@@ -37,9 +37,6 @@ struct simp_config {
     bool                      m_beta;
     bool                      m_eta;
     bool                      m_proj;
-    /* The following option should be removed as soon as we
-       refactor the inductive compiler. */
-    bool                      m_use_matcher{true};
     simp_config();
     simp_config(vm_obj const & o);
 };