From 60ac0b508dc3206c411f94b5b46373bea4a23796 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Dec 2013 21:14:22 -0800 Subject: [PATCH] fix(tests/kernel/environment): adjust the test to reflect (recent) change in the normalizer Signed-off-by: Leonardo de Moura --- src/tests/kernel/environment.cpp | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index a18db9e0d..f6889831a 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -101,13 +101,8 @@ static void tst3() { lean_assert(normalize(Const("b"), c_env) == iVal(6)); c_env->add_definition("c", Int, Const("a")); lean_assert(normalize(Const("c"), c_env) == iVal(3)); - try { - expr r = normalize(Const("c"), env); - lean_assert(r == iVal(3)); - lean_unreachable(); - } catch (exception const & ex) { - std::cout << "expected error: " << ex.what() << std::endl; - } + expr r = normalize(Const("c"), env); + lean_assert(r == Const("c")); std::cout << "end tst3" << std::endl; }