From 50183ce7200d6059b4146c0cc4933aa524178c02 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 12 Oct 2015 15:39:20 +0200
Subject: Univs: be more restrictive for template polymorphic constants: only
 direct aliases are ok, and indices should not be made polymorphic. Fixes
 NFix.

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

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a02d5e2055..1f8706652f 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -165,10 +165,7 @@ 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
-	  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)
+          make (cons_subst u s 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