From 131853c16169c7fc3d479dfc15b25d9d03c93237 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:12:12 +0100
Subject: [PATCH] Adapt to coq/coq#18331 (mind_kelim -> mind_squashed)

---
 src/coq_elpi_builtins.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 423ac1e5c..c8f8b683c 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -1612,10 +1612,7 @@ informative, as well a singleton types in Prop (which are
 regarded as not non-informative).|})),
   (fun i ~depth {env} _ state ->
       let _, indbo = Inductive.lookup_mind_specif env i in
-      match indbo.Declarations.mind_kelim with
-      | (Sorts.InSProp | Sorts.InProp) -> raise No_clause
-      | Sorts.InSet when Environ.is_impredicative_set env -> raise No_clause
-      | (Sorts.InSet | Sorts.InType | Sorts.InQSort) -> ()
+      if Option.has_some indbo.Declarations.mind_squashed then raise No_clause
     )),
   DocAbove);