diff options
| author | Pierre-Marie Pédrot | 2020-01-11 15:40:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-11 15:40:23 +0100 |
| commit | cea51c865f52841b02d64da06f04b29f893a8d4a (patch) | |
| tree | f24fae36c4c98442a9bf45db61aae35e1b3c5eb7 /kernel/indTyping.ml | |
| parent | 8a5e3cd84ab077f0bbe57bd13dca750cda043bf4 (diff) | |
| parent | e1da46b1141e1fc9ce04f2285fbb50fe3aab18b7 (diff) | |
Merge PR #11367: Minor cleanup of indtypes/indtyping
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/indTyping.ml')
| -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 |