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).

---
 library/declare.ml   |  1 +
 library/universes.ml | 11 +++++++----
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index fb6e1c9b81..56c789c1ed 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -353,6 +353,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
   mind_entry_arity = mkProp;
+  mind_entry_template = false;
   mind_entry_consnames = mie.mind_entry_consnames;
   mind_entry_lc = []
 }
diff --git a/library/universes.ml b/library/universes.ml
index 438e6cc532..d69386ddf9 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -957,10 +957,13 @@ let is_direct_sort_constraint s v = match s with
 let solve_constraints_system levels level_bounds level_min =
   let open Univ in
   let levels =
-    Array.map (Option.map
-		 (fun u -> match Universe.level u with 
-		 | Some u -> u 
-		 | _ -> Errors.anomaly (Pp.str"expects Atom")))
+    Array.mapi (fun i o ->
+      match o with
+      | Some u ->
+	(match Universe.level u with 
+	| Some u -> Some u 
+	| _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
+      | None -> None)
       levels in
   let v = Array.copy level_bounds in
   let nind = Array.length v in
-- 
cgit v1.2.3