From f1884ee5f9a8aaf68272a0b555094b732673e73a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Jul 2014 13:22:32 -0700 Subject: [PATCH] chore(frontends/lean): remove dead code Signed-off-by: Leonardo de Moura --- src/frontends/lean/hint_table.h | 13 ------------- 1 file changed, 13 deletions(-) delete mode 100644 src/frontends/lean/hint_table.h diff --git a/src/frontends/lean/hint_table.h b/src/frontends/lean/hint_table.h deleted file mode 100644 index 723a78907..000000000 --- a/src/frontends/lean/hint_table.h +++ /dev/null @@ -1,13 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/rb_map.h" -#include "library/tactic/tactic.h" - -namespace lean { -typedef rb_map hint_table; -}