From b3d97c2147418f44fc704807d3812b04921591af Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 15:36:57 +0200
Subject: Univs: fix bug #4251, handling of template polymorphic constants.

---
 kernel/inductive.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 87c139f48d..a02d5e2055 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -165,7 +165,10 @@ let rec make_subst env =
         (* to be greater than the level of the argument; this is probably *)
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
-        make (cons_subst u s subst) (sign, exp, args)
+	  if Univ.Universe.is_levels s then
+            make (cons_subst u s subst) (sign, exp, args)
+	  else (* Cannot handle substitution by i+n universes. *)
+	    make subst (sign, exp, args)
     | (na,None,t)::sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
-- 
cgit v1.2.3