michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(build): C++ module dependency problem, and style

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-14 18:29:51 -08:00
parent c8e1ec87d2
commit 28eb980484
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/frontend.cpp
View file

@ -20,6 +20,7 @@ Author: Leonardo de Moura
#include "kernel/builtin.h" #include "kernel/builtin.h"
#include "kernel/io_state.h" #include "kernel/io_state.h"
#include "library/io_state_stream.h" #include "library/io_state_stream.h"
#include "library/ite.h"
#include "library/expr_pair.h" #include "library/expr_pair.h"
#include "library/expr_pair_maps.h" #include "library/expr_pair_maps.h"
#include "library/arith/nat.h" #include "library/arith/nat.h"
@ -569,6 +570,7 @@ io_state init_frontend(environment const & env, bool no_kernel) {
io_state init_test_frontend(environment const & env) { io_state init_test_frontend(environment const & env) {
env->set_trusted_imported(true); env->set_trusted_imported(true);
io_state ios = init_frontend(env); io_state ios = init_frontend(env);
import_ite(env, ios);
import_int(env, ios); import_int(env, ios);
import_real(env, ios); import_real(env, ios);
return ios; return ios;

1
src/library/kernel_bindings.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include <utility> #include <utility>
#include <string>
#include "util/sstream.h" #include "util/sstream.h"
#include "util/script_state.h" #include "util/script_state.h"
#include "kernel/expr.h" #include "kernel/expr.h"