From 33dd168195cf561786163adce7e471f82f011aeb Mon Sep 17 00:00:00 2001
From: Nicolas Braud-Santoni <nicolas@braud-santoni.eu>
Date: Tue, 22 Aug 2017 18:09:57 +0000
Subject: [PATCH] Remove unnecessary parameter

---
 src/tactic/core/injectivity_tactic.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp
index 75685c891..4dc3fe5d5 100644
--- a/src/tactic/core/injectivity_tactic.cpp
+++ b/src/tactic/core/injectivity_tactic.cpp
@@ -268,7 +268,6 @@ public:
     virtual void collect_param_descrs(param_descrs & r) {
         insert_max_memory(r);
         insert_produce_models(r);
-        r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier.");
     }
     
     virtual void operator()(goal_ref const & g,