From 2ebf8ab8f17396bbb11293889b5d6da4ccf9aeb7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 18 May 2018 13:19:22 -0700
Subject: [PATCH] chore(*): unnecessary `#include`s

---
 src/frontends/lean/calc.cpp                | 1 -
 src/frontends/lean/elaborator.cpp          | 1 -
 src/frontends/lean/inductive_cmds.cpp      | 1 -
 src/frontends/lean/info_manager.cpp        | 1 -
 src/frontends/lean/pp.cpp                  | 1 -
 src/frontends/lean/user_command.cpp        | 1 -
 src/library/constructions/brec_on.cpp      | 1 -
 src/library/constructions/cases_on.cpp     | 1 -
 src/library/constructions/no_confusion.cpp | 1 -
 src/library/constructions/rec_on.cpp       | 1 -
 10 files changed, 10 deletions(-)

diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp
index 63c26f2771..5cbacbb3d0 100644
--- a/src/frontends/lean/calc.cpp
+++ b/src/frontends/lean/calc.cpp
@@ -20,7 +20,6 @@ Author: Leonardo de Moura
 #include "library/choice.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
-#include "library/scoped_ext.h"
 #include "library/annotation.h"
 #include "library/sorry.h"
 #include "frontends/lean/parser.h"
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3729c73551..d8c136189a 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -36,7 +36,6 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/private.h"
 #include "library/attribute_manager.h"
-#include "library/scoped_ext.h"
 #include "library/protected.h"
 #include "library/message_builder.h"
 #include "library/aliases.h"
diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index 3202acb1ab..dd568bc6c6 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -17,7 +17,6 @@ Authors: Daniel Selsam, Leonardo de Moura
 #include "kernel/inductive/inductive.h"
 #include "kernel/abstract.h"
 #include "kernel/free_vars.h"
-#include "library/scoped_ext.h"
 #include "library/locals.h"
 #include "library/attribute_manager.h"
 #include "library/deep_copy.h"
diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index 0a58b9cad6..7a32317b8e 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/trace.h"
 #include "library/documentation.h"
-#include "library/scoped_ext.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_format.h"
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index b3fe9ddffe..39f529b181 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -19,7 +19,6 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 #include "library/aliases.h"
 #include "library/class.h"
-#include "library/scoped_ext.h"
 #include "library/expr_pair.h"
 #include "library/placeholder.h"
 #include "library/private.h"
diff --git a/src/frontends/lean/user_command.cpp b/src/frontends/lean/user_command.cpp
index f717d5e3f8..c26a899a76 100644
--- a/src/frontends/lean/user_command.cpp
+++ b/src/frontends/lean/user_command.cpp
@@ -8,7 +8,6 @@ Author: Sebastian Ullrich
 #include "kernel/abstract.h"
 #include "library/constants.h"
 #include "library/attribute_manager.h"
-#include "library/scoped_ext.h"
 #include "library/tactic/elaborator_exception.h"
 #include "library/string.h"
 #include "library/vm/vm_expr.h"
diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp
index b5054d3c89..bdbe5988f4 100644
--- a/src/library/constructions/brec_on.cpp
+++ b/src/library/constructions/brec_on.cpp
@@ -18,7 +18,6 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/normalize.h"
 #include "library/aux_recursors.h"
-#include "library/scoped_ext.h"
 #include "library/constructions/util.h"
 
 namespace lean {
diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp
index 9f930290f7..7e963a2e35 100644
--- a/src/library/constructions/cases_on.cpp
+++ b/src/library/constructions/cases_on.cpp
@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/normalize.h"
 #include "library/aux_recursors.h"
-#include "library/scoped_ext.h"
 #include "library/constructions/util.h"
 
 namespace lean {
diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp
index 05726e7543..a565e5abcf 100644
--- a/src/library/constructions/no_confusion.cpp
+++ b/src/library/constructions/no_confusion.cpp
@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/constants.h"
 #include "library/normalize.h"
-#include "library/scoped_ext.h"
 #include "library/aux_recursors.h"
 #include "library/constructions/util.h"
 
diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp
index ff0c9d09c8..9b2437c7e6 100644
--- a/src/library/constructions/rec_on.cpp
+++ b/src/library/constructions/rec_on.cpp
@@ -16,7 +16,6 @@ Author: Leonardo de Moura
 #include "library/protected.h"
 #include "library/normalize.h"
 #include "library/aux_recursors.h"
-#include "library/scoped_ext.h"
 #include "library/constructions/util.h"
 
 namespace lean {