From 7056c27774f3420942325d1f59c9fe63a930e41b Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Wed, 8 Jan 2025 14:09:38 -0800
Subject: [PATCH] chore: remove Environment extensions for the old compiler

---
 src/Lean/Compiler/Old.lean | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean
index 52908bc84eda..66f79ad1a2e3 100644
--- 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