diff --git a/tests/lean/run/blast16.lean b/tests/lean/run/blast16.lean index bf8aa232f7..b3bdcb0ca4 100644 --- a/tests/lean/run/blast16.lean +++ b/tests/lean/run/blast16.lean @@ -1,6 +1,4 @@ -set_option blast.init_depth 10 -set_option blast.inc_depth 100 -set_option blast.trace true +set_option trace.blast true example (p q : Prop) : p ∨ q → q ∨ p := by blast diff --git a/tests/lean/run/simplifier1.lean b/tests/lean/run/simplifier1.lean index daedc6317f..d127cd37bb 100644 --- a/tests/lean/run/simplifier1.lean +++ b/tests/lean/run/simplifier1.lean @@ -4,7 +4,7 @@ attribute P_sub [instance] constant q : P → nat → Prop set_option blast.simp false -set_option blast.trace true +set_option trace.blast true set_option trace.congruence_closure true example (a : nat) (h₁ h₂ : P) : q h₁ a = q h₂ a :=