diff --git a/src/Lean/ErrorExplanations.lean b/src/Lean/ErrorExplanations.lean
index 422b78b4f8..11883115bc 100644
--- a/src/Lean/ErrorExplanations.lean
+++ b/src/Lean/ErrorExplanations.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.ErrorExplanations.CtorResultingTypeMismatch
 public import Lean.ErrorExplanations.DependsOnNoncomputable
+public import Lean.ErrorExplanations.InductionWithNoAlts
 public import Lean.ErrorExplanations.InductiveParamMismatch
 public import Lean.ErrorExplanations.InductiveParamMissing
 public import Lean.ErrorExplanations.InferBinderTypeFailed