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 96abc1b commit e7d2354Copy full SHA for e7d2354
src/Lean/ExtraModUses.lean
@@ -44,7 +44,7 @@ public def getExtraModUses (env : Environment) (modIdx : ModuleIdx) : Array Extr
44
/-- Copies additional recorded import dependencies from one environment to another. -/
45
public def copyExtraModUses (src dest : Environment) : Environment := Id.run do
46
let mut env := dest
47
- for entry in extraModUses.getEntries src do
+ for entry in extraModUses.getEntries (asyncMode := .local) src do
48
if !(extraModUses.getState (asyncMode := .local) env).contains entry then
49
env := extraModUses.addEntry env entry
50
env
0 commit comments