From 750691bd5adead11e293ce673a5812ed894868ef Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 3 Apr 2021 18:24:03 -0700
Subject: [PATCH] chore: fix tests

---
 tests/lean/infoTree.lean.expected.out   |  2 ++
 tests/lean/namedHoles.lean.expected.out | 10 +++++-----
 tests/lean/rewrite.lean.expected.out    |  2 +-
 3 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index 0d2945f46a..364a3a8c25 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -166,6 +166,8 @@
           | (z, w) =>
             let z1 : Nat := z + w;
             z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩
+            [.] `z : none
+            [.] `w : none
             (z, w) : Nat × Nat @ ⟨23, 8⟩-⟨23, 14⟩
               Macro expansion
               (z, w)
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index 4cea1eb4d7..1882413c52 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/tests/lean/namedHoles.lean.expected.out
@@ -1,15 +1,15 @@
 namedHoles.lean:9:7-9:14: error: application type mismatch
-  f ?m ?m
+  f ?x ?x
 argument
-  ?m
+  ?x
 has type
   Nat : Type
 but is expected to have type
   Bool : Type
-g ?m ?m : Nat
+g ?x ?x : Nat
 20
-foo (fun (x : Nat) => ?m x) ?m : Nat
-bla ?m fun (x : Nat) => ?m : Nat
+foo (fun (x : Nat) => ?m x) ?hole : Nat
+bla ?hole fun (x : Nat) => ?hole : Nat
 namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
 boo (fun (x : Nat) => ?m x) fun (y : Bool) => sorry : Nat
 11
diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out
index b71e7b3ff8..bf0bd63de4 100644
--- a/tests/lean/rewrite.lean.expected.out
+++ b/tests/lean/rewrite.lean.expected.out
@@ -2,7 +2,7 @@
 as bs : List α
 ⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
 rewrite.lean:12:20-12:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
-  List.reverse (List.reverse ?m)
+  List.reverse (List.reverse ?as)
 α : Type u_1
 as bs : List α
 ⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)