diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 1175b39ce651..0895dbedf21b 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -294,7 +294,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     modify fun s => { s with messages := {} };
     pure messages
   let restoreMessages (prevMessages : MessageLog) : CommandElabM Unit := do
-    modify fun s => { s with messages := prevMessages ++ s.messages.errorsToWarnings }
+    modify fun s => { s with messages := prevMessages ++ s.messages.errorsToInfos }
   let prevMessages ← resetMessages
   let succeeded ← try
     x
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 15618a0ba69f..94f9916431e7 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -448,6 +448,9 @@ def markAllReported (log : MessageLog) : MessageLog :=
 def errorsToWarnings (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
 
+def errorsToInfos (log : MessageLog) : MessageLog :=
+  { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.information } | _ => m) }
+
 def getInfoMessages (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
 
diff --git a/tests/lean/run/autoLift.lean b/tests/lean/run/autoLift.lean
index 649378804b08..a054b2c6d8be 100644
--- a/tests/lean/run/autoLift.lean
+++ b/tests/lean/run/autoLift.lean
@@ -19,7 +19,7 @@ set_option autoLift false
 
 set_option pp.mvars false in
 /--
-warning: type mismatch
+info: type mismatch
   f
 has type
   IO Nat : Type