From 29fc39c9510b0d865dd4ad0092fc7d1324a4c971 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 4 Apr 2024 15:42:01 +0200 Subject: [PATCH] Adapt to coq/coq#18867 (inductive_sort_family doesn't exist) --- template-coq/src/quoter.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml index 6e5f6e136..28802d76c 100644 --- a/template-coq/src/quoter.ml +++ b/template-coq/src/quoter.ml @@ -441,9 +441,12 @@ struct in ps, acc | _ -> [], acc in + (* TODO quote the real squash data instead of approximating with a sort family *) let kelim = match oib.Declarations.mind_squashed with | None -> Sorts.InType - | Some _ -> Inductive.inductive_sort_family oib + | Some _ -> match oib.mind_arity with + | TemplateArity _ -> InType + | RegularArity s -> Sorts.family s.mind_sort in let sf = Q.quote_sort_family kelim in (Q.quote_ident oib.mind_typename, indices, indsort, indty, sf,