X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=1f92a5fa881b95396c1eaf06fd2a06fdcc0fc1fc;hb=d7ed0cc36dd7e4169bc8f37b5b58884a17de4a89;hp=6065d24bd41a705fba4f977ea28dd18b919c9300;hpb=f495c35ee3660fa7b602feb570d99e56e570b711;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 6065d24bd..1f92a5fa8 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -1182,7 +1182,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* we search a coercion from hety to s *) let coer, tgt_carr = let carr t subst context = - CicMetaSubst.apply_subst subst t + CicReduction.whd ~delta:false + context (CicMetaSubst.apply_subst subst t ) in let c_hety = carr hety subst context in let c_s = carr s subst context in @@ -1645,3 +1646,5 @@ let type_of_aux' ?localization_tbl metasenv context term ugraph = let typecheck ~localization_tbl metasenv uri obj = profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj + +let _ = DoubleTypeInference.pack_coercion := pack_coercion;;