From 172b3f67308f7011a4ad6431f232853d4f224af1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 3 Feb 2025 15:44:08 +0100
Subject: [PATCH] fix

---
 Lean4CheckerTests/AddFalse.lean            | 14 ++++++++++++--
 Lean4CheckerTests/AddFalseConstructor.lean | 14 ++++++++++++--
 Lean4CheckerTests/ReplaceAxiom.lean        | 15 +++++++++++++--
 3 files changed, 37 insertions(+), 6 deletions(-)

diff --git a/Lean4CheckerTests/AddFalse.lean b/Lean4CheckerTests/AddFalse.lean
index 1ac1550..ca4be68 100644
--- a/Lean4CheckerTests/AddFalse.lean
+++ b/Lean4CheckerTests/AddFalse.lean
@@ -1,6 +1,9 @@
 import Lean4CheckerTests.OpenPrivate
 
-open private mk from Lean.Environment
+open private Lean.Environment.mk from Lean.Environment
+open private Lean.Kernel.Environment.mk from Lean.Environment
+open private Lean.Kernel.Environment.extensions from Lean.Environment
+open private Lean.Kernel.Environment.extraConstNames from Lean.Environment
 
 open Lean in
 elab "add_false" : command => do
@@ -9,7 +12,14 @@ elab "add_false" : command => do
       { name := `false, levelParams := [], type := .const ``False [], value := .const ``False [] }
     -- Before `Environment.mk` became private, we could just use
     -- `{ env with constants }`
-    mk env.const2ModIdx constants env.extensions env.extraConstNames env.header
+    let kenv := Lean.Kernel.Environment.mk constants
+      env.toKernelEnv.quotInit
+      env.toKernelEnv.diagnostics
+      env.toKernelEnv.const2ModIdx
+      (Lean.Kernel.Environment.extensions env.toKernelEnv)
+      (Lean.Kernel.Environment.extraConstNames env.toKernelEnv)
+      env.header
+    Lean.Environment.mk kenv (.pure kenv) {} none
 
 add_false
 
diff --git a/Lean4CheckerTests/AddFalseConstructor.lean b/Lean4CheckerTests/AddFalseConstructor.lean
index 9968da3..1b33ade 100644
--- a/Lean4CheckerTests/AddFalseConstructor.lean
+++ b/Lean4CheckerTests/AddFalseConstructor.lean
@@ -1,6 +1,9 @@
 import Lean4CheckerTests.OpenPrivate
 
-open private mk from Lean.Environment
+open private Lean.Environment.mk from Lean.Environment
+open private Lean.Kernel.Environment.mk from Lean.Environment
+open private Lean.Kernel.Environment.extensions from Lean.Environment
+open private Lean.Kernel.Environment.extraConstNames from Lean.Environment
 
 open Lean in
 elab "add_false_constructor" : command => do
@@ -16,7 +19,14 @@ elab "add_false_constructor" : command => do
         isUnsafe := false }
     -- Before `Environment.mk` became private, we could just use
     -- `{ env with constants }`
-    mk env.const2ModIdx constants env.extensions env.extraConstNames env.header
+    let kenv := Lean.Kernel.Environment.mk constants
+      env.toKernelEnv.quotInit
+      env.toKernelEnv.diagnostics
+      env.toKernelEnv.const2ModIdx
+      (Lean.Kernel.Environment.extensions env.toKernelEnv)
+      (Lean.Kernel.Environment.extraConstNames env.toKernelEnv)
+      env.header
+    Lean.Environment.mk kenv (.pure kenv) {} none
 
 add_false_constructor
 
diff --git a/Lean4CheckerTests/ReplaceAxiom.lean b/Lean4CheckerTests/ReplaceAxiom.lean
index 62a675e..5c5cbcb 100644
--- a/Lean4CheckerTests/ReplaceAxiom.lean
+++ b/Lean4CheckerTests/ReplaceAxiom.lean
@@ -1,8 +1,12 @@
 import Lean4CheckerTests.OpenPrivate
 
+open private Lean.Environment.mk from Lean.Environment
+open private Lean.Kernel.Environment.mk from Lean.Environment
+open private Lean.Kernel.Environment.extensions from Lean.Environment
+open private Lean.Kernel.Environment.extraConstNames from Lean.Environment
+
 /- Redefine `propext : False`. -/
 open Lean Elab Meta in
-open private Environment.mk from Lean.Environment in
 #eval modifyEnv (m := MetaM) fun env =>
   let consts :=
     { env.constants with
@@ -13,7 +17,14 @@ open private Environment.mk from Lean.Environment in
           isUnsafe := false
         })
     }
-  Lean.Environment.mk env.const2ModIdx consts env.extensions env.extraConstNames env.header
+  let kenv := Lean.Kernel.Environment.mk consts
+    env.toKernelEnv.quotInit
+    env.toKernelEnv.diagnostics
+    env.toKernelEnv.const2ModIdx
+    (Lean.Kernel.Environment.extensions env.toKernelEnv)
+    (Lean.Kernel.Environment.extraConstNames env.toKernelEnv)
+    env.header
+  Lean.Environment.mk kenv (.pure kenv) {} none
 
 theorem efsq : ∀ (x y z n : Nat),
     0 < x → 0 < y → 0 < z → 2 < n →