Skip to content

Commit 0297f94

Browse files
committed
fix tests
1 parent da091fc commit 0297f94

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

tests/lean/interactive/incrementalTactic.lean.expected.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ t 2
3434
"severity": 1,
3535
"range":
3636
{"start": {"line": 1, "character": 38}, "end": {"line": 4, "character": 3}},
37-
"message": "unexpected token '/-!'; expected ')', '_', identifier or term",
37+
"message": "unexpected token '/-!'; expected term",
3838
"fullRange":
3939
{"start": {"line": 1, "character": 38},
4040
"end": {"line": 4, "character": 3}}}]}

tests/lean/parserRecovery.lean.expected.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ parserRecovery.lean:49:30-49:36: error: unexpected token; expected identifier
3636
parserRecovery.lean:50:9-50:11: error: unexpected token ')'; expected term
3737
parserRecovery.lean:69:16-69:17: error: unexpected token ']'; expected '|}'
3838
parserRecovery.lean:69:20: error: unexpected token at this precedence level; consider parenthesizing the term
39-
parserRecovery.lean:72:15-72:16: error: unexpected token ']'; expected ')', ',' or ':'
39+
parserRecovery.lean:72:15-72:16: error: unexpected token ']'; expected ')'
4040
parserRecovery.lean:100:3-101:1: error: unexpected token; expected identifier
4141
parserRecovery.lean:103:1-104:3: error: unexpected token 'def'; expected identifier
4242
parserRecovery.lean:105:0-105:1: error: unexpected token; expected identifier

0 commit comments

Comments
 (0)