From e59735bde93ce877592425faeb8494de39aca856 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Aug 2020 10:20:57 -0700 Subject: [PATCH] chore: fix test @Kha the tests `Reparen.lean` and `Reformat.lean` are still broken. Could you please take a look? They broke because I changed the `match` syntax at 3ce794c58. --- tests/compiler/termparsertest1.lean.expected.out | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out index 3857bb9fb3..f643aef3df 100644 --- a/tests/compiler/termparsertest1.lean.expected.out +++ b/tests/compiler/termparsertest1.lean.expected.out @@ -230,7 +230,7 @@ match x with | none => false (Term.match "match" - [(Term.id `x [])] + [[] (Term.id `x [])] [] "with" ["|"] @@ -246,7 +246,7 @@ match x with (Term.match "match" - [(Term.id `x [])] + [[] (Term.id `x [])] [] "with" ["|"] @@ -255,7 +255,7 @@ match x with "=>" (Term.match "match" - [(Term.id `y [])] + [[] (Term.id `y [])] [] "with" ["|"]