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 /library/universes.mli | |
| parent | 7e4925b78162226331c65ef77f2da681a0b8ee48 (diff) | |
Cleanup code related to the constraint solving, which sits now outside the
kernel in library/universes.ml.
Diffstat (limited to 'library/universes.mli')
| -rw-r--r-- | library/universes.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/library/universes.mli b/library/universes.mli index 5b0951928..2fc476732 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -243,3 +243,8 @@ val minimize_univ_variables : Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints + +(** {6 Support for old-style sort-polymorphism } *) + +val solve_constraints_system : universe option array -> universe array -> universe array -> + universe array |