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