From 43ce35985b1ecd88efc8cfa8ec16f72c1ca6b231 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Oct 2020 16:47:34 -0700
Subject: [PATCH] chore: fix test

---
 src/Lean/Elab/Term.lean         | 2 ++
 tests/lean/run/doNotation2.lean | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 75b1c49044..d264d9e778 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1290,6 +1290,8 @@ fun stx expectedType? =>
     refTermType ← inferType refTerm;
     e ← elabTerm (stx.getArg 3) expectedType?;
     eType ← inferType e;
+    -- TODO: try coercions. We cannot simply use `ensureHasType` at this point because it has no support for the custom error message.
+    -- a `catch` would also not work since `ensureHasType` may postpone the coercion resolution.
     unlessM (isDefEq eType refTermType) $ throwError $ mkTypeMismatchError e eType refTermType msg;
     pure e
 
diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index f098312ae5..854e625536 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -78,7 +78,7 @@ def find? (xs : List Nat) (p : Nat → Bool) : Option Nat := Id.run do
 let result := none
 for x in xs do
   if p x then
-    result := x
+    result := some x
     break
 return result