diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-03 23:45:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-03 23:45:01 +0200 |
| commit | 23d30ddc2a7cdfa3f71e99f57d36818b16ad40b7 (patch) | |
| tree | bdd895f74d2764e4e57a1c4aab65ba4408442190 /toplevel/command.ml | |
| parent | 7e4925b78162226331c65ef77f2da681a0b8ee48 (diff) | |
Cleanup code related to the constraint solving, which sits now outside the
kernel in library/universes.ml.
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 = |