From 5ee7a211cf24ac307a0b4dfbdf6b556c978ce28f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 May 2019 17:47:39 -0700 Subject: [PATCH] chore(tests/lean/run/rc_tests): fix test --- tests/lean/run/rc_tests.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/rc_tests.lean b/tests/lean/run/rc_tests.lean index 2263c1eefb..99fea49844 100644 --- a/tests/lean/run/rc_tests.lean +++ b/tests/lean/run/rc_tests.lean @@ -3,7 +3,7 @@ universes u v -- setOption pp.binderTypes False set_option pp.implicit true set_option trace.compiler.llnf true -set_option trace.compiler.boxed true +-- set_option trace.compiler.boxed true namespace x1