From 1220aab80893b68c14adb64ba0b75811961ac04d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Dec 2019 13:03:31 +0100
Subject: minor cleanup template_polymorphic_univs: check_levels returns bool

---
 kernel/indTyping.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'kernel/indTyping.ml')

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index d9ccf81619..b19472dc99 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -197,16 +197,14 @@ let unbounded_from_below u cstrs =
    is u_k and is contributing. *)
 let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl =
   let check_level l =
-    if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
-       unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
-       not (Univ.LSet.mem l ctor_levels) then
-      Some l
-    else None
+    Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+    unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
+    not (Univ.LSet.mem l ctor_levels)
   in
   let univs = Univ.Universe.levels concl in
   let univs =
     if template_check then
-      Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs
+      Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
     else univs (* Doesn't check the universes can be generalized *)
   in
   let fold acc = function
-- 
cgit v1.2.3