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.ml | |
| 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.ml')
| -rw-r--r-- | pretyping/termops.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9888821d14..cd848984d4 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -146,11 +146,12 @@ let print_env env = let set_module m = current_module := m*) -let new_univ = +let new_univ_level = let univ_gen = ref 0 in (fun sp -> incr univ_gen; - Univ.make_univ (Lib.library_dp(),!univ_gen)) + Univ.make_universe_level (Lib.library_dp(),!univ_gen)) +let new_univ () = Univ.make_universe (new_univ_level ()) let new_Type () = mkType (new_univ ()) let new_Type_sort () = Type (new_univ ()) |