Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 1 addition & 3 deletions src/Lean/CoreM.lean
Original file line number Diff line number Diff line change
Expand Up @@ -708,9 +708,7 @@ def compileDeclsImpl (declNames : Array Name) : CoreM Unit := do

-- `ref?` is used for error reporting if available
partial def compileDecls (decls : Array Name) (logErrors := true) : CoreM Unit := do
-- When inside `realizeConst`, do compilation synchronously so that `_cstage*` constants are found
-- by the replay code
if !Elab.async.get (← getOptions) || (← getEnv).isRealizing then
if !Elab.async.get (← getOptions) then
let _ ← traceBlock "compiler env" (← getEnv).checked
doCompile
return
Expand Down
2 changes: 1 addition & 1 deletion src/Lean/Meta/Match/MatchEqs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -229,7 +229,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
assert! matchInfo.altInfos == splitterAltInfos
-- This match statement does not need a splitter, we can use itself for that.
-- (We still have to generate a declaration to satisfy the realizable constant)
addAndCompile <| Declaration.defnDecl {
addAndCompile (logCompileErrors := false) <| Declaration.defnDecl {
name := splitterName
levelParams := constInfo.levelParams
type := constInfo.type
Expand Down
Loading