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

fix(library/kernel_bindings): g++ compilation error

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-02 14:34:33 -07:00
parent 4fddc5b8bc
commit b83410f042
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/constraint.h
View file

@ -32,7 +32,7 @@ namespace lean {
It means, t must be definitionally equal to one of the terms in the (finite)
set {s_1, ..., s_k}.
*/
enum constraint_kind { Eq, Convertible, Level, Choice };
enum class constraint_kind { Eq, Convertible, Level, Choice };
struct constraint_cell;
class constraint {
constraint_cell * m_ptr;

4
src/library/kernel_bindings.cpp
View file

@ -1000,7 +1000,7 @@ CNSTR_PRED(is_level_cnstr)
CNSTR_PRED(is_choice_cnstr)
static int constraint_eq(lua_State * L) { return push_boolean(L, to_constraint(L, 1) == to_constraint(L, 2)); }
static int constraint_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_constraint(L, 1), to_constraint(L, 2))); }
static int constraint_kind(lua_State * L) { return push_integer(L, static_cast<int>(to_constraint(L, 1).kind())); }
static int constraint_get_kind(lua_State * L) { return push_integer(L, static_cast<int>(to_constraint(L, 1).kind())); }
static int constraint_hash(lua_State * L) { return push_integer(L, to_constraint(L, 1).hash()); }
static int constraint_jst(lua_State * L) { return push_justification(L, to_constraint(L, 1).get_justification()); }
static int constraint_lhs(lua_State * L) {
@ -1043,7 +1043,7 @@ static const struct luaL_Reg constraint_m[] = {
{"is_level", safe_function<constraint_is_level_cnstr>},
{"is_choice", safe_function<constraint_is_choice_cnstr>},
{"is_eqp", safe_function<constraint_is_eqp>},
{"kind", safe_function<constraint_kind>},
{"kind", safe_function<constraint_get_kind>},
{"hash", safe_function<constraint_hash>},
{"lhs", safe_function<constraint_lhs>},
{"rhs", safe_function<constraint_rhs>},