From b3577d942307c3a23aabd224a588af16a0337094 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 Aug 2018 10:59:29 +0200
Subject: Elaboration: do not ask poly inductives to be template

---
 vernac/comInductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 0ca1bfd0c0..d23784f774 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -423,7 +423,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
   let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) -> {
     mind_entry_typename = ind.ind_name;
     mind_entry_arity = arity;
-    mind_entry_template = Option.cata (fun s -> not (Sorts.is_small s)) false concl;
+    mind_entry_template = not poly && Option.cata (fun s -> not (Sorts.is_small s)) false concl;
     mind_entry_consnames = cnames;
     mind_entry_lc = ctypes
   }) indl arities arityconcl constructors in
-- 
cgit v1.2.3