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)