max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/run/rc_tests): fix test

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-22 17:47:39 -07:00
parent 3e76e43843
commit 5ee7a211cf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/rc_tests.lean
View file

@ -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