From 2df6f0358cc153e42b52ca68b1cd0d64dda1cb2d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 3 Jun 2017 18:47:48 +0200 Subject: [PATCH] fix(library/vm/vm_parser): header worries after rebase --- src/library/vm/vm_parser.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index 62977635bf..d2caabfc4c 100644 --- a/src/library/vm/vm_parser.cpp +++ b/src/library/vm/vm_parser.cpp @@ -4,25 +4,27 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich */ +#include "library/vm/vm_parser.h" #include #include #include -#include "library/type_context.h" +#include "library/constants.h" +#include "library/explicit.h" #include "library/num.h" #include "library/quote.h" #include "library/trace.h" -#include "library/tactic/tactic_evaluator.h" -#include "library/explicit.h" +#include "library/vm/interaction_state_imp.h" #include "library/tactic/elaborate.h" -#include "library/vm/vm.h" #include "library/vm/vm_string.h" +#include "library/vm/vm_options.h" +#include "library/vm/vm_environment.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_nat.h" -#include "library/vm/vm_parser.h" +#include "library/vm/vm_name.h" #include "library/vm/vm_pos_info.h" -#include "library/vm/interaction_state_imp.h" #include "frontends/lean/info_manager.h" #include "frontends/lean/elaborator.h" +#include "frontends/lean/parser.h" #include "util/utf8.h" namespace lean { @@ -57,7 +59,7 @@ expr parse_interactive_param(parser & p, expr const & param_ty) { vm_obj vm_parsed = run_parser(p, param_args[2]); type_context ctx(p.env()); name n("_reflect"); - tactic_evaluator eval(ctx, p.get_options(), param_args[0]); + lean_parser::evaluator eval(ctx, p.get_options()); auto env = eval.compile(n, param_args[1]); vm_state S(env, p.get_options()); auto vm_res = S.invoke(n, vm_parsed);