diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 6b383e41b4..8930d6ac6c 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -142,7 +142,7 @@ match d with | Decl.fdecl f xs t b => do unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code"); env ← getEnv; - let usesLeanAPI := usesModuleFrom env `Init.Lean; + let usesLeanAPI := usesModuleFrom env `Lean; if usesLeanAPI then emitLn "void lean_initialize();" else