From dc7696652ccd23887a474f3d4141b1850e51d46f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 19:50:00 +0200 Subject: Remove unused argument to solve_constraints_system --- vernac/comInductive.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/comInductive.ml') 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 -> -- cgit v1.2.3