diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index b170ee6..a38775c 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -26,6 +26,8 @@ protected def Info.stx? : Info → Option Syntax
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
   | .ofOmissionInfo       info => info.stx
+  | .ofChoiceInfo         info => info.stx
+  | .ofPartialTermInfo    info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 protected def Info.isOriginal (i : Info) : Bool :=
   match i.stx? with
@@ -141,6 +143,8 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
       | .ofFVarAliasInfo _ => pure "[fvar]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
       | .ofOmissionInfo _ => pure "[omission]"
+      | .ofChoiceInfo _ => pure "[choice]"
+      | .ofPartialTermInfo  _ => pure "[partial_term]"
       let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
       return s!"{node}\n{children}"
     else throw <| IO.userError "No `ContextInfo` available."
diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean
index 0b4719f..c0cdcc1 100644
--- a/Pantograph/Tactic/Prograde.lean
+++ b/Pantograph/Tactic/Prograde.lean
@@ -40,7 +40,7 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
   let fvarId ← mkFreshFVarId
   let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
   let mvarUpstream ←
-    withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+    Meta.withLCtx lctxUpstream #[] do
       Meta.withNewLocalInstances #[.fvar fvarId] 0 do
         let mvarUpstream ← mkUpstreamMVar mvarId
         --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
diff --git a/flake.lock b/flake.lock
index 9f54bbe..4a17f3d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,16 +42,15 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1733351931,
-        "narHash": "sha256-ngMjY/ci6490G2gofaS9CODtpnmFoYzfaI13U14TkFM=",
+        "lastModified": 1736388194,
+        "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "157c85903f668fadeb79f330961b7bbe5ee596de",
+        "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
         "type": "github"
       },
       "original": {
         "owner": "lenianiva",
-        "ref": "157c85903f668fadeb79f330961b7bbe5ee596de",
         "repo": "lean4-nix",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 1dfc515..af6e4fb 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix?ref=157c85903f668fadeb79f330961b7bbe5ee596de";
+    lean4-nix.url = "github:lenianiva/lean4-nix";
     lspec = {
       url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
       flake = false;
@@ -18,19 +18,9 @@
     lean4-nix,
     lspec,
     ...
-  } : flake-parts.lib.mkFlake { inherit inputs; } {
-    flake = {
-    };
-    systems = [
-      "aarch64-linux"
-      "aarch64-darwin"
-      "x86_64-linux"
-      "x86_64-darwin"
-    ];
-    perSystem = { system, pkgs, ... }: let
-      pkgs = import nixpkgs {
-        inherit system;
-        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      flake = {
       };
       systems = [
         "aarch64-linux"
@@ -94,7 +84,6 @@
           inherit (repl) executable;
           default = repl.executable;
         };
-        formatter = pkgs.alejandra;
         legacyPackages = {
           inherit project;
           leanPkgs = pkgs.lean;
@@ -108,6 +97,7 @@
               ${test.executable}/bin/test > $out
             '';
         };
+        formatter = pkgs.alejandra;
         devShells.default = pkgs.mkShell {
           buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
         };
diff --git a/lean-toolchain b/lean-toolchain
index 1e70935..d0eb99f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0
+leanprover/lean4:v4.15.0