diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indTyping.ml | 10 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 21 |
2 files changed, 14 insertions, 17 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 diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ab915e2b8d..0d900c2ec9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -487,18 +487,17 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in - let transf num = - let arity = List.length (dest_subterms recarg).(num) in - if Int.equal arity 0 then - let p = (!nconst, 0) in - incr nconst; p - else - let p = (!nblock + 1, arity) in - incr nblock; p - (* les tag des constructeur constant commence a 0, - les tag des constructeur non constant a 1 (0 => accumulator) *) + let transf arity = + if Int.equal arity 0 then + let p = (!nconst, 0) in + incr nconst; p + else + let p = (!nblock + 1, arity) in + incr nblock; p + (* les tag des constructeur constant commence a 0, + les tag des constructeur non constant a 1 (0 => accumulator) *) in - let rtbl = Array.init (List.length cnames) transf in + let rtbl = Array.map transf consnrealargs in (* Build the inductive packet *) { mind_typename = id; mind_arity = arity; |