diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-11 17:19:32 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-11 17:19:32 +0000 |
| commit | e35e8be666ae2513ada6da416326b1e7534fb201 (patch) | |
| tree | 2309dd2600b7e946bb4712950687dec428e52fcb /plugins/subtac | |
| 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 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 28bf6e64d..509a4e9e5 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -159,9 +159,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let c = constr_of_global ref in make_judge c (Retyping.get_type_of env Evd.empty c) - let pretype_sort = function + let pretype_sort evdref = function | GProp c -> judge_of_prop_contents c - | GType _ -> judge_of_new_Type () + | GType _ -> evd_comb0 judge_of_new_Type evdref let split_tycon_lam loc env evd tycon = let rec real_split evd c = @@ -307,7 +307,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct inh_conv_coerce_to_tycon loc env evdref fixj tycon | GSort (loc,s) -> - inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon + let s' = pretype_sort evdref s in + inh_conv_coerce_to_tycon loc env evdref s' tycon | GApp (loc,f,args) -> let length = List.length args in |