From 50323e5b1433ab1d4307a23dbabfb980ba93d3d4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Dec 2015 12:30:20 -0800 Subject: [PATCH] fix(tests/lean/run/simplifier1): option name --- tests/lean/run/simplifier1.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/simplifier1.lean b/tests/lean/run/simplifier1.lean index d127cd37bb..71cbec0edc 100644 --- a/tests/lean/run/simplifier1.lean +++ b/tests/lean/run/simplifier1.lean @@ -5,7 +5,7 @@ constant q : P → nat → Prop set_option blast.simp false set_option trace.blast true -set_option trace.congruence_closure true +set_option trace.cc true example (a : nat) (h₁ h₂ : P) : q h₁ a = q h₂ a := by blast