fix

Author: Rob23oba

src/Lean/Elab/ErrorExplanation.lean

@@ -103,7 +103,7 @@ open Command in
 | `(registerErrorExplanationStx| $docStx:docComment register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do
   unless (← getEnv).contains ``ErrorExplanation.Metadata do
     throwError "To use this command, add `import Lean.ErrorExplanation` to the header of this file"
-  withoutExporting <| recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := true)
+  recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := true)
   let tp := mkConst ``ErrorExplanation.Metadata
   let metadata ← runTermElabM <| fun _ => unsafe do
     let e ← elabTermEnsuringType t tp

tests/lean/run/extraModUses.lean

@@ -233,7 +233,7 @@ register_error_explanation lean.never {
 }
 
 /--
-info: Entries: [import Lean.ErrorExplanation]
+info: Entries: [meta import Lean.ErrorExplanation]
 Is rev mod use: false
 -/
 #guard_msgs in #eval showExtraModUses