We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 0601dd2 commit 7ca84efCopy full SHA for 7ca84ef
src/Lean/Elab/ErrorExplanation.lean
@@ -103,7 +103,7 @@ open Command in
103
| `(registerErrorExplanationStx| $docStx:docComment register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do
104
unless (← getEnv).contains ``ErrorExplanation.Metadata do
105
throwError "To use this command, add `import Lean.ErrorExplanation` to the header of this file"
106
- recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := false)
+ withoutExporting <| recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := true)
107
let tp := mkConst ``ErrorExplanation.Metadata
108
let metadata ← runTermElabM <| fun _ => unsafe do
109
let e ← elabTermEnsuringType t tp
0 commit comments