diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 19:50:00 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
| commit | dc7696652ccd23887a474f3d4141b1850e51d46f (patch) | |
| tree | dec58e3326e0cc0787e29792fac820e37627a7ae /vernac/comInductive.ml | |
| parent | a7153b347f8196122394e9ce912055cdf9e575ae (diff) | |
Remove unused argument to solve_constraints_system
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7d7f9e23f..5da96a855 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -202,7 +202,7 @@ let is_direct_sort_constraint s v = match s with | Some u -> Univ.univ_level_mem u v | None -> false -let solve_constraints_system levels level_bounds level_min = +let solve_constraints_system levels level_bounds = let open Univ in let levels = Array.mapi (fun i o -> @@ -273,7 +273,7 @@ let inductive_levels env evd poly arities inds = (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) let levels' = solve_constraints_system (Array.of_list levels) - (Array.of_list cstrs_levels) (Array.of_list min_levels) + (Array.of_list cstrs_levels) in let evd, arities = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> |