diff options
| author | Gaëtan Gilbert | 2019-12-30 13:03:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-07 10:15:45 +0100 |
| commit | 1220aab80893b68c14adb64ba0b75811961ac04d (patch) | |
| tree | a9eecd12c75e8b33cc5b0d9d9d4a3369e67c9d48 | |
| parent | a7de863bf68f6aae3832e8c8d5b000576d107a63 (diff) | |
minor cleanup template_polymorphic_univs: check_levels returns bool
| -rw-r--r-- | kernel/indTyping.ml | 10 |
1 files changed, 4 insertions, 6 deletions
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 |