From 262f962e4fd3cec5c5075468be4c8433f17f136e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 Aug 2018 11:03:17 +0200
Subject: Elaboration: do not ask for small records to be template

Imitating the kernel in anticipation for the kernel being more obedient
---
 vernac/record.ml | 5 +++++
 1 file changed, 5 insertions(+)

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;
-- 
cgit v1.2.3