diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index 15c2aef6d..2cae0e143 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -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; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index f0cdc04f4..dd166d850 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -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(to_constraint(L, 1).kind())); } +static int constraint_get_kind(lua_State * L) { return push_integer(L, static_cast(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}, {"is_choice", safe_function}, {"is_eqp", safe_function}, - {"kind", safe_function}, + {"kind", safe_function}, {"hash", safe_function}, {"lhs", safe_function}, {"rhs", safe_function},