chore: remove Environment extensions for the old compiler

leanprover · Jan 12, 2025 · 7056c27 · 7056c27
1 parent 9e3bc9c
commit 7056c27
Showing 1 changed file with 0 additions and 15 deletions.
diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean
@@ -53,18 +53,3 @@ def isUnsafeRecName? : Name → Option Name
   | _ => none
 
 end Compiler
-
-namespace Environment
-
-/--
-Compile the given block of mutual declarations.
-Assumes the declarations have already been added to the environment using `addDecl`.
--/
-@[extern "lean_compile_decls"]
-opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment
-
-/-- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/
-def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
-  compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
-
-end Environment