diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 4fc574daf..ff2e89351 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -413,7 +413,7 @@ let inductive_levels env evdref poly arities inds = in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) - let levels' = Univ.solve_constraints_system (Array.of_list levels) + let levels' = Universes.solve_constraints_system (Array.of_list levels) (Array.of_list cstrs_levels) (Array.of_list min_levels) in let evd = |