diff options
| author | Gaëtan Gilbert | 2020-11-04 13:16:55 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-16 11:24:56 +0100 |
| commit | 41840f92c0ee8c10691411f2a44e4059a4754456 (patch) | |
| tree | a53f6ea3edef5c4ee10d90baab656ce8323ba312 | |
| parent | 779d2b915a970cdfc87d3d1b69e10bab04094f33 (diff) | |
Small cleanup in ComInductive
| -rw-r--r-- | vernac/comInductive.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index bb26ce652e..cc3f7bc093 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -271,9 +271,8 @@ let inductive_levels env evd arities inds = if Sorts.is_prop a || Sorts.is_sprop a then None else Some (univ_of_sort a)) destarities in - let cstrs_levels, min_levels, sizes = - CList.split3 - (List.map2 (fun (_,tys) (arity,(ctx,du)) -> + let cstrs_levels, sizes = + CList.split (List.map2 (fun (_,tys) (arity,(ctx,du)) -> let len = List.length tys in let minlev = Sorts.univ_of_sort du in let minlev = @@ -283,13 +282,15 @@ let inductive_levels env evd arities inds = in let minlev = (* Indices contribute. *) - if indices_matter env && List.length ctx > 0 then ( + if indices_matter env then begin let ilev = sign_level env evd ctx in - Univ.sup ilev minlev) + Univ.sup ilev minlev + end else minlev in let clev = extract_level env evd minlev tys in - (clev, minlev, len)) inds destarities) + (clev, len)) + inds destarities) in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) |