From 23d30ddc2a7cdfa3f71e99f57d36818b16ad40b7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 3 Jul 2014 23:45:01 +0200
Subject: Cleanup code related to the constraint solving, which sits now
 outside the kernel in library/universes.ml.

---
 kernel/indtypes.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index cc56428fa4..ee4a404a7c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -320,7 +320,6 @@ let typecheck_inductive env ctx mie =
 	in
 	  match s with
 	  | Type u when expltype (* Explicitly polymorphic *) ->
-	      (* && no_upper_constraints u (Univ.UContext.constraints mie.mind_entry_universes) -> *)
 	    (* The polymorphic level is a function of the level of the *)
 	    (* conclusions of the parameters *)
             (* We enforce [u >= lev] in case [lev] has a strict upper *)
-- 
cgit v1.2.3