From bcc8b6759231c608623db5eb70296fa0bda6f9cd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Dec 2013 12:40:52 -0800 Subject: [PATCH] chore(*): consistent file name convention Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp.cpp | 2 +- src/kernel/abstract.cpp | 2 +- src/kernel/free_vars.cpp | 2 +- src/kernel/instantiate.cpp | 2 +- src/kernel/{replace.h => replace_fn.h} | 0 src/kernel/replace_visitor.h | 2 +- src/library/elaborator/elaborator.cpp | 2 +- src/library/rewriter/rewriter.cpp | 2 +- src/library/rewriter/rewriter.h | 2 +- src/library/substitution.cpp | 2 +- src/library/tactic/goal.cpp | 2 +- src/tests/kernel/replace.cpp | 2 +- 12 files changed, 11 insertions(+), 11 deletions(-) rename src/kernel/{replace.h => replace_fn.h} (100%) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 282869e46..e01d859fb 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -20,7 +20,7 @@ Author: Leonardo de Moura #include "kernel/occurs.h" #include "kernel/builtin.h" #include "kernel/free_vars.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "library/context_to_lambda.h" #include "library/placeholder.h" #include "frontends/lean/notation.h" diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index c3366087e..6bb20cbcf 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include "kernel/abstract.h" #include "kernel/free_vars.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" namespace lean { expr abstract(expr const & e, unsigned n, expr const * s) { diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index a8ef36817..1dfc229f4 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include #include "kernel/free_vars.h" #include "kernel/expr_sets.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "kernel/metavar.h" namespace lean { diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index b5a5ce512..343590f01 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include #include "kernel/free_vars.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "kernel/metavar.h" namespace lean { diff --git a/src/kernel/replace.h b/src/kernel/replace_fn.h similarity index 100% rename from src/kernel/replace.h rename to src/kernel/replace_fn.h diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index b3c95508d..9f402543b 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "util/scoped_map.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "kernel/context.h" namespace lean { diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 18b718376..11a98fd82 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -13,7 +13,7 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" #include "kernel/normalizer.h" #include "kernel/instantiate.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "kernel/builtin.h" #include "library/type_inferer.h" #include "library/update_expr.h" diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index 023148efb..a2529c5b2 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/src/library/rewriter/rewriter.cpp @@ -12,7 +12,7 @@ #include "kernel/environment.h" #include "kernel/expr.h" #include "kernel/printer.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "library/basic_thms.h" #include "library/rewriter/fo_match.h" #include "library/rewriter/rewriter.h" diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h index f7a67ce6a..478200335 100644 --- a/src/library/rewriter/rewriter.h +++ b/src/library/rewriter/rewriter.h @@ -13,7 +13,7 @@ Author: Soonho Kong #include "kernel/context.h" #include "kernel/environment.h" #include "kernel/expr.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "library/basic_thms.h" #include "library/rewriter/rewriter.h" #include "library/type_inferer.h" diff --git a/src/library/substitution.cpp b/src/library/substitution.cpp index fead6d5d6..21402682d 100644 --- a/src/library/substitution.cpp +++ b/src/library/substitution.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "kernel/metavar.h" #include "library/substitution.h" #include "library/kernel_bindings.h" diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 92e8cbc47..941dfe51f 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "util/name_set.h" #include "util/buffer.h" #include "kernel/for_each_fn.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "kernel/abstract.h" #include "library/kernel_bindings.h" #include "library/type_inferer.h" diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp index 77b61b3fb..30ffc9306 100644 --- a/src/tests/kernel/replace.cpp +++ b/src/tests/kernel/replace.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/expr_maps.h" -#include "kernel/replace.h" +#include "kernel/replace_fn.h" #include "kernel/printer.h" #include "library/deep_copy.h" using namespace lean;