Adapt to coq/coq#18331 (mind_kelim -> mind_squashed)

SkySkimmer · Nov 20, 2023 · 98b5e34 · 98b5e34
1 parent d0d8403
commit 98b5e34
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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