fix

leanprover · Feb 3, 2025 · 172b3f6 · 172b3f6
1 parent 764cf7e
commit 172b3f6
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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 →