From 98b5e3492934794aa7a5729df9c02954ec9a3b37 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 20 Nov 2023 15:17:16 +0100
Subject: [PATCH] Adapt to coq/coq#18331 (mind_kelim -> mind_squashed)

---
 src/lean.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lean.ml b/src/lean.ml
index 429b9c0..9bad8c6 100644
--- a/src/lean.ml
+++ b/src/lean.ml
@@ -1019,7 +1019,7 @@ and declare_ind n { params; ty; ctors; univs } i =
       in
       assert (
         squashy.lean_squashes
-        || (Global.lookup_mind mind).mind_packets.(0).mind_kelim == InType);
+        || (Global.lookup_mind mind).mind_packets.(0).mind_squashed == None);
       (mind, algs, ind_name, cnames, univs, squashy)
   in