chore: disable injectivity theorems generation for big structure tests

The test was producing a stack overflow in debug mode in CI.
2021-05-15 21:27:58 -07:00 · 2021-05-15 21:27:58 -07:00 · a498a64490
commit a498a64490
parent 5d305faee0
2 changed files with 2 additions and 0 deletions
--- a/tests/compiler/bigctor.lean
+++ b/tests/compiler/bigctor.lean
@ -1,3 +1,4 @@
+set_option genInjectivity false
 structure Foo where
  x1  : Nat := 0
  x2  : Nat := 0
--- a/tests/lean/run/bigctor.lean
+++ b/tests/lean/run/bigctor.lean
@ -1,3 +1,4 @@
+set_option genInjectivity false
 structure Foo where
  x1  : Nat := 0
  x2  : Nat := 0