diff --git a/tests/lean/unfold_crash.lean b/tests/lean/unfold_crash.lean index edfc48e9f..45329abfa 100644 --- a/tests/lean/unfold_crash.lean +++ b/tests/lean/unfold_crash.lean @@ -4,6 +4,6 @@ open nat example (a b : nat) : a = succ b → a = b + 1 := begin intro h, - try (unfold succ at h) + try (unfold succ at h), unfold succ at h end diff --git a/tests/lean/unfold_crash.lean.expected.out b/tests/lean/unfold_crash.lean.expected.out index 1e2d2e56d..750468112 100644 --- a/tests/lean/unfold_crash.lean.expected.out +++ b/tests/lean/unfold_crash.lean.expected.out @@ -1 +1 @@ -unfold_crash.lean:8:2: error: invalid 'begin-end' expression, ',' expected +unfold_crash.lean:8:9: error: invalid 'unfold', 'nat.succ' is not a definition