From 4481b95f6f89acd7013b16a345d379dc44d67705 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 5 Mar 2020 15:14:47 +0100
Subject: Template polymorphism is now a property of the inductive block.

For an inductive block to be template, all its components must also
be. This is probably fixing a few soundness bugs in the process, but I
do not want to think too much about it.
---
 kernel/entries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8d930b521c..983fa822e9 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -37,7 +37,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
   mind_entry_arity : constr;
-  mind_entry_template : bool; (* Use template polymorphism *)
   mind_entry_consnames : Id.t list;
   mind_entry_lc : constr list }
 
@@ -50,6 +49,7 @@ type mutual_inductive_entry = {
   mind_entry_params : Constr.rel_context;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : universes_entry;
+  mind_entry_template : bool; (* Use template polymorphism *)
   mind_entry_cumulative : bool;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
-- 
cgit v1.2.3