diff options
| author | msozeau | 2011-03-11 17:19:32 +0000 |
|---|---|---|
| committer | msozeau | 2011-03-11 17:19:32 +0000 |
| commit | e35e8be666ae2513ada6da416326b1e7534fb201 (patch) | |
| tree | 2309dd2600b7e946bb4712950687dec428e52fcb /pretyping/termops.mli | |
| parent | 7a97fcc78a73ab36d0cb1526397b4d2d7299ed34 (diff) | |
Tentative to make unification check types at every instanciation of an
evar, and simultaneously make type inference with universes work better.
This only exports more functions from kernel/univ, to be able to work
with a set of universe variables during type inference. Universe
constraints are gradually added during type checking, adding information
necessary e.g. to lower the level of unknown Type variables to Prop or
Set. There does not seem to be a disastrous performance hit on the
stdlib, but might have one on some contribs (hence the "Tentative").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 1350743d5d..71e781aeb8 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -14,6 +14,7 @@ open Sign open Environ (** Universes *) +val new_univ_level : unit -> Univ.universe_level val new_univ : unit -> Univ.universe val new_sort_in_family : sorts_family -> sorts val new_Type : unit -> types |