From e35e8be666ae2513ada6da416326b1e7534fb201 Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 11 Mar 2011 17:19:32 +0000 Subject: 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 --- plugins/subtac/subtac_pretyping_F.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'plugins/subtac') 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 -- cgit v1.2.3