From 8d6c1cc32ccdfc0aeaa40978a81464467cc59712 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:36:11 +0100
Subject: [PATCH] Adapt to coq/coq#18331 (mind_kelim -> mind_squashed)

---
 template-coq/src/quoter.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
index 7e63684a5..12d96db52 100644
--- a/template-coq/src/quoter.ml
+++ b/template-coq/src/quoter.ml
@@ -429,7 +429,11 @@ struct
                 in ps, acc
             | _ -> [], acc
           in
-          let sf = Q.quote_sort_family oib.Declarations.mind_kelim in
+          let kelim = match oib.Declarations.mind_squashed with
+            | None -> Sorts.InType
+            | Some _ -> Inductive.inductive_sort_family oib
+          in
+          let sf = Q.quote_sort_family kelim in
             (Q.quote_ident oib.mind_typename, indices, indsort, indty, sf,
              (List.rev reified_ctors), projs, Q.quote_relevance oib.mind_relevance) :: ls, acc)
         ([],acc) (Array.to_list mib.mind_packets)