From ff0a051caf031fb427007714f6325c74b8893702 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Nov 2014 19:34:25 +0100
Subject: Pass around information on the use of template polymorphism for
 inductive types (i.e., ones declared with an explicit anonymous Type at the
 conclusion of their arity). With this change one can force inductives to live
 in higher universes even in the non-fully universe polymorphic case (e.g. bug
 #3821).

---
 kernel/entries.mli | 3 ++-
 kernel/indtypes.ml | 9 +++++----
 2 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.mli b/kernel/entries.mli
index f6958849b0..baeec31b4b 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -37,6 +37,7 @@ 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 }
 
@@ -48,7 +49,7 @@ type mutual_inductive_entry = {
   mind_entry_finite : Decl_kinds.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
-  mind_entry_polymorphic : bool;
+  mind_entry_polymorphic : bool; 
   mind_entry_universes : Univ.universe_context;
   mind_entry_private : bool option }
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index afd7cde979..6dd3ab2ba9 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -226,7 +226,8 @@ let typecheck_inductive env ctx mie =
     List.fold_left
       (fun (env_ar,l) ind ->
          (* Arities (without params) are typed-checked here *)
-         let arity, expltype = 
+	 let expltype = ind.mind_entry_template in
+         let arity =
 	   if isArity ind.mind_entry_arity then
 	     let (ctx,s) = dest_arity env_params ind.mind_entry_arity in
 	       match s with
@@ -237,12 +238,12 @@ let typecheck_inductive env ctx mie =
 	         let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in
 		 let (cctx, _) = destArity proparity.utj_val in
 		   (* Any universe is well-formed, we don't need to check [s] here *)
-		   mkArity (cctx, s), not (Sorts.is_small s)
+		   mkArity (cctx, s)
 	       | _ -> 
 		 let arity = infer_type env_params ind.mind_entry_arity in
-		   arity.utj_val, not (Sorts.is_small s)
+		   arity.utj_val
 	   else let arity = infer_type env_params ind.mind_entry_arity in
-		  arity.utj_val, false
+		  arity.utj_val
 	 in
 	 let (sign, deflev) = dest_arity env_params arity in
 	 let inflev = 
-- 
cgit v1.2.3