added a whd (nodelta) in the carr function used by the refiner (in the eat_prods...

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 6065d24bd41a705fba4f977ea28dd18b919c9300..1f92a5fa881b95396c1eaf06fd2a06fdcc0fc1fc 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/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;;