diff options
| -rw-r--r-- | vernac/record.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 6b5c538df2..af4fd0846c 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -417,6 +417,11 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in + let template = + template && + let _, s = Reduction.dest_arity (Global.env()) arity in + not (Sorts.is_small s) + in { mind_entry_typename = id; mind_entry_arity = arity; mind_entry_template = template; |