From b1777855cf9bb2caf55b02f5b2b4729f5a357b56 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Nov 2015 11:45:20 -0800 Subject: [PATCH] chore(util/rb_multi_map): remove unnecessary includes --- src/util/rb_multi_map.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/util/rb_multi_map.h b/src/util/rb_multi_map.h index b33f97961..c0a0f9c2f 100644 --- a/src/util/rb_multi_map.h +++ b/src/util/rb_multi_map.h @@ -6,8 +6,6 @@ Author: Daniel Selsam #pragma once #include "util/rb_map.h" #include "util/list.h" -#include "kernel/expr.h" -#include "library/io_state_stream.h" namespace lean {