Merge pull request #14 from SkySkimmer/sort-poly-ind

SkySkimmer · Nov 29, 2023 · 1036369 · 1036369
2 parents d0d8403 + 98b5e34
commit 1036369
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