From 862795e9e9e303d15a3aaaf95a2dd78e2f19bf2d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 May 2020 14:57:29 -0700 Subject: [PATCH] fix: `usesLeanAPI` --- src/Lean/Compiler/IR/EmitC.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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