diff --git a/tests/compiler/bigctor.lean b/tests/compiler/bigctor.lean index 1206779290..84bd189bf8 100644 --- 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 diff --git a/tests/lean/run/bigctor.lean b/tests/lean/run/bigctor.lean index b14a8e8b2c..fd8d32b2c0 100644 --- 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