From 560e7af1287ede8146da77cdc4674c29598744bf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 8 Sep 2019 13:33:51 +0200 Subject: [PATCH] fix(library/init/lean/compiler/ir/compilerm): borrow annotations on extern decls do not do anything right now --- library/init/lean/compiler/ir/compilerm.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/compiler/ir/compilerm.lean b/library/init/lean/compiler/ir/compilerm.lean index 4057f32bf7..0efb451c79 100644 --- a/library/init/lean/compiler/ir/compilerm.lean +++ b/library/init/lean/compiler/ir/compilerm.lean @@ -92,7 +92,7 @@ registerSimplePersistentEnvExtension { constant declMapExt : SimplePersistentEnvExtension Decl DeclMap := default _ @[export lean_ir_find_env_decl] -def findEnvDecl (env : @& Environment) (n : @& Name) : Option Decl := +def findEnvDecl (env : Environment) (n : Name) : Option Decl := (declMapExt.getState env).find n def findDecl (n : Name) : CompilerM (Option Decl) :=