diff --git a/tests/lean/CompilerFindJoinPoints.lean.expected.out b/tests/lean/CompilerFindJoinPoints.lean.expected.out index 9b58e211af..4df1bda51c 100644 --- a/tests/lean/CompilerFindJoinPoints.lean.expected.out +++ b/tests/lean/CompilerFindJoinPoints.lean.expected.out @@ -1,3 +1,4 @@ + [Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 [Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 successful [Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurence 0 diff --git a/tests/lean/run/inlineApp.lean b/tests/lean/run/inlineApp.lean index edc720fbdb..85f8377ca7 100644 --- a/tests/lean/run/inlineApp.lean +++ b/tests/lean/run/inlineApp.lean @@ -10,7 +10,7 @@ def h (x : Nat) := open Lean Compiler LCNF in @[cpass] def simpInline : PassInstaller := - Testing.assertDoesNotContainConstAfter `simp `simpInlinesInline ``inline "simp did not inline `inline`" + Testing.assertDoesNotContainConstAfter ``inline "simp did not inline `inline`" |>.install `simp `simpInlinesInline set_option trace.Compiler.result true #eval Lean.Compiler.compile #[``h]