From fabfe32ca5dc7fa0006e74dc3abe0cc1f40aed74 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Sep 2018 12:05:29 -0700 Subject: [PATCH] chore(*): remove unnecessary `scoped_ext` dependencies --- src/frontends/lean/builtin_cmds.cpp | 1 - src/frontends/lean/builtin_exprs.cpp | 1 - src/frontends/lean/decl_cmds.cpp | 1 - src/frontends/lean/decl_util.cpp | 1 - src/frontends/lean/definition_cmds.cpp | 1 - src/frontends/lean/json.cpp | 1 - src/frontends/lean/notation_cmd.cpp | 1 - src/frontends/lean/parser.cpp | 1 - src/frontends/lean/structure_cmd.cpp | 1 - src/frontends/lean/util.cpp | 1 - src/library/aux_recursors.cpp | 1 - src/library/constructions/projection.cpp | 1 - src/library/derive_attribute.cpp | 1 - src/library/tactic/tactic_state.cpp | 1 - 14 files changed, 14 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 09d5cf1025..8c1dc67952 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -15,7 +15,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "library/eval_helper.h" -#include "library/scoped_ext.h" #include "library/trace.h" #include "library/aliases.h" #include "library/export_decl.h" diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 06a2af23cd..35b52f126f 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/explicit.h" #include "library/aliases.h" -#include "library/scoped_ext.h" #include "library/constants.h" #include "library/string.h" #include "library/trace.h" diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index a2f0ae992d..0c6d0fb68e 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/replace_fn.h" #include "kernel/for_each_fn.h" -#include "library/scoped_ext.h" #include "library/aliases.h" #include "library/private.h" #include "library/protected.h" diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 90d5962512..fbecd36b0c 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -18,7 +18,6 @@ Author: Leonardo de Moura #include "library/aliases.h" #include "library/explicit.h" #include "library/reducible.h" -#include "library/scoped_ext.h" #include "frontends/lean/util.h" #include "frontends/lean/decl_util.h" #include "frontends/lean/tokens.h" diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 1dc7dfecd5..7f3c0e9113 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -21,7 +21,6 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/private.h" #include "library/protected.h" -#include "library/scoped_ext.h" #include "library/noncomputable.h" #include "library/module.h" #include "library/aux_definition.h" diff --git a/src/frontends/lean/json.cpp b/src/frontends/lean/json.cpp index c028cb1459..1dc7d06609 100644 --- a/src/frontends/lean/json.cpp +++ b/src/frontends/lean/json.cpp @@ -7,7 +7,6 @@ Author: Gabriel Ebner #ifdef LEAN_JSON #include "frontends/lean/json.h" #include -#include "library/scoped_ext.h" #include "library/protected.h" #include "kernel/declaration.h" #include "library/type_context.h" diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 03bccdc10c..7eaefcff0d 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include "runtime/utf8.h" #include "kernel/abstract.h" #include "kernel/replace_fn.h" -#include "library/scoped_ext.h" #include "library/explicit.h" #include "library/num.h" #include "library/aliases.h" diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 385470616e..4d27c43c45 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -37,7 +37,6 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/deep_copy.h" #include "library/module.h" -#include "library/scoped_ext.h" #include "library/explicit.h" #include "library/num.h" #include "library/string.h" diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index c7388f6b15..1c6595543b 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -21,7 +21,6 @@ Author: Leonardo de Moura #include "library/replace_visitor.h" #include "library/trace.h" #include "library/attribute_manager.h" -#include "library/scoped_ext.h" #include "library/placeholder.h" #include "library/locals.h" #include "library/reducible.h" diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index a10944bb0b..a501b89799 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/for_each_fn.h" #include "library/error_msgs.h" -#include "library/scoped_ext.h" #include "library/annotation.h" #include "library/locals.h" #include "library/explicit.h" diff --git a/src/library/aux_recursors.cpp b/src/library/aux_recursors.cpp index 497fc987e6..fad0970e26 100644 --- a/src/library/aux_recursors.cpp +++ b/src/library/aux_recursors.cpp @@ -7,7 +7,6 @@ Author: Leonardo de Moura #include #include "library/aux_recursors.h" #include "library/constants.h" -#include "library/scoped_ext.h" #include "library/module.h" namespace lean { diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index c173b6e849..a818c409ee 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -15,7 +15,6 @@ Author: Leonardo de Moura #include "library/projection.h" #include "library/module.h" #include "library/util.h" -#include "library/scoped_ext.h" #include "library/class.h" #include "library/constructions/projection.h" #include "library/constructions/util.h" diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp index 3493693fa3..ca064d4fb7 100644 --- a/src/library/derive_attribute.cpp +++ b/src/library/derive_attribute.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "runtime/sstream.h" #include "kernel/find_fn.h" #include "library/util.h" -#include "library/scoped_ext.h" #include "library/user_recursors.h" #include "library/aux_recursors.h" #include "library/attribute_manager.h" diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 540e8167fa..9b1667c56c 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "library/cache_helper.h" #include "library/module.h" #include "library/check.h" -#include "library/scoped_ext.h" #include "library/aux_definition.h" #include "library/vm/vm_format.h" #include "library/vm/vm_string.h"