diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 6db18e4182..63474f773e 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -324,6 +324,7 @@ unsafe def elabEvalUnsafe : CommandElab
     let elabEvalTerm : TermElabM Expr := do
       let e ← Term.elabTerm term none
       Term.synthesizeSyntheticMVarsNoPostponing
+      if (← Term.logUnassignedUsingErrorInfos (← getMVars e)) then throwAbortTerm
       if (← isProp e) then
         mkDecide e
       else
diff --git a/tests/lean/evalNone.lean b/tests/lean/evalNone.lean
new file mode 100644
index 0000000000..f83f87b4f5
--- /dev/null
+++ b/tests/lean/evalNone.lean
@@ -0,0 +1,3 @@
+#eval none
+
+#eval [].head?
diff --git a/tests/lean/evalNone.lean.expected.out b/tests/lean/evalNone.lean.expected.out
new file mode 100644
index 0000000000..7fdcd9ce11
--- /dev/null
+++ b/tests/lean/evalNone.lean.expected.out
@@ -0,0 +1,12 @@
+evalNone.lean:1:6-1:10: error: don't know how to synthesize implicit argument
+  @none ?m
+context:
+⊢ Type ?u
+evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
+  @List.head? ?m []
+context:
+⊢ Type ?u
+evalNone.lean:3:6-3:8: error: don't know how to synthesize implicit argument
+  @List.nil ?m
+context:
+⊢ Type ?u
diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
index 3a24ada2c6..350971fecd 100644
--- a/tests/lean/evalWithMVar.lean.expected.out
+++ b/tests/lean/evalWithMVar.lean.expected.out
@@ -2,10 +2,10 @@ Sum.someRight c : Option Nat
 evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
   @c ?m
 context:
-⊢ Type u_1
+⊢ Type ?u
 evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
   @Sum.someRight ?m Nat c
 context:
-⊢ Type u_1
+⊢ Type ?u
 Sum.someRight c : Option Nat
 Sum.someRight c : Option Nat