From 42b5e780f564dae04758235fb410fc1b1bf40a38 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Jan 2021 08:14:16 -0800 Subject: [PATCH] chore: fix test --- tests/lean/docStr.lean.expected.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out index 7d9fd3ffb8..a38713277b 100644 --- a/tests/lean/docStr.lean.expected.out +++ b/tests/lean/docStr.lean.expected.out @@ -82,5 +82,5 @@ namedPattern := { range := { pos := { line := 166, column := 13 }, endPos := { line := 166, column := 61 } }, selectionRange := { pos := { line := 166, column := 17 }, endPos := { line := 166, column := 29 } } } Lean.Meta.forallTelescopeReducing := - { range := { pos := { line := 663, column := 0 }, endPos := { line := 664, column := 58 } }, - selectionRange := { pos := { line := 663, column := 4 }, endPos := { line := 663, column := 27 } } } + { range := { pos := { line := 668, column := 0 }, endPos := { line := 669, column := 58 } }, + selectionRange := { pos := { line := 668, column := 4 }, endPos := { line := 668, column := 27 } } }