From cc9a1be62f55738915fc2a24d9560796acde719e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9ana=20=E6=B1=9F?= <leana.jiang+git@icloud.com>
Date: Sun, 25 Jan 2026 22:01:04 +0100
Subject: [PATCH] npins/cornelis: use 2.7.1 due to agda's interface change

---
 nix/overlays/cornelis.nix | 5 +++++
 npins/sources.json        | 9 +++++----
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/nix/overlays/cornelis.nix b/nix/overlays/cornelis.nix
index 7ae3c175..3008001b 100644
--- a/nix/overlays/cornelis.nix
+++ b/nix/overlays/cornelis.nix
@@ -2,4 +2,9 @@
 let
   sources = import ../../npins;
 in
+
+# If this is updated, we break split on case support for PLFA.
+# PLFA uses 2.7.0
+# https://github.com/agda/cornelis/issues/169
+assert sources.cornelis.version == "v2.7.1";
 sources.cornelis.asFlake.overlays.cornelis
diff --git a/npins/sources.json b/npins/sources.json
index 929ec7c3..c6de909e 100644
--- a/npins/sources.json
+++ b/npins/sources.json
@@ -27,10 +27,11 @@
       "version_upper_bound": null,
       "release_prefix": null,
       "submodules": false,
-      "version": "v2.8.0",
-      "revision": "67137c76fe0d4a8bb899eea46afaa370993d3556",
-      "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.8.0",
-      "hash": "sha256-dGS6De3EtTirgEMDMSjA+iBNc670W7pG4eA02Nq7Azo="
+      "version": "v2.7.1",
+      "revision": "40298eed11eb877526b3ab3f648d8a7bff9e2f50",
+      "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.7.1",
+      "hash": "sha256-h18AeggnOSSjy0RLJIkWsSID1BJTarOV9F1APKusIrE=",
+      "frozen": true
     },
     "disko": {
       "type": "GitRelease",