From f79e46a8a038b8ee996009b4430a98f08bcb82ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 Jul 2016 10:39:34 -0700 Subject: [PATCH] fix(frontends/lean/old_elaborator): remove "old" [intro] --- src/frontends/lean/old_attributes.cpp | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/frontends/lean/old_attributes.cpp b/src/frontends/lean/old_attributes.cpp index 3974fceb00..ae210ba14c 100644 --- a/src/frontends/lean/old_attributes.cpp +++ b/src/frontends/lean/old_attributes.cpp @@ -37,14 +37,6 @@ void initialize_old_attributes() { [](environment const & env, name const & n) { return LEAN_DEFAULT_PRIORITY; }); - register_prio_attribute("intro", "introduction rule for backward chaining", - [](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) { - return env; - }, - [](environment const &, name const &) { return false; }, - [](environment const & env, name const & d) { - return LEAN_DEFAULT_PRIORITY; - }); } void finalize_old_attributes() {} }