diff options
| -rw-r--r-- | kernel/univ.ml | 21 | ||||
| -rw-r--r-- | toplevel/command.ml | 2 |
2 files changed, 22 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index b42de5a760..6a11251b06 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1700,9 +1700,30 @@ let solve_constraints_system levels level_bounds level_min = levels in let v = Array.copy level_bounds in let nind = Array.length v in + let clos = Array.map (fun _ -> Int.Set.empty) levels in + (* First compute the transitive closure of the levels dependencies *) for i=0 to nind-1 do for j=0 to nind-1 do if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then + clos.(i) <- Int.Set.add j clos.(i); + done; + done; + let rec closure () = + let continue = ref false in + Array.iteri (fun i deps -> + let deps' = + Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps + in + if Int.Set.equal deps deps' then () + else (clos.(i) <- deps'; continue := true)) + clos; + if !continue then closure () + else () + in + closure (); + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && Int.Set.mem j clos.(i) then (v.(i) <- Universe.sup v.(i) level_bounds.(j); level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) done; diff --git a/toplevel/command.ml b/toplevel/command.ml index 95ddf1fb06..4fc574daf5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -390,7 +390,7 @@ let sup_list = List.fold_left Univ.sup Univ.type0m_univ let extract_level env evd tys = let sorts = List.map (fun ty -> let ctx, concl = Reduction.dest_prod_assum env ty in - sign_level env evd ctx) tys + sign_level env evd ((Anonymous, None, concl) :: ctx)) tys in sup_list sorts let inductive_levels env evdref poly arities inds = |