X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=90643164d576bf14b5f309fc4011104bfa1d8b1b;hb=3df775cea96aae2d25dd9b47f9491711abc1c8fb;hp=e99ce5cd70285fe94680b80fdab6a20442b860c7;hpb=9151b08e0041e0e8d4823a92dbc12e120d6075f6;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index e99ce5cd7..90643164d 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1197,7 +1197,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       function
         | [] -> [],metasenv,subst,hetype,ugraph
         | (hete, hety)::tl ->
-            (match hetype with
+	    (match (CicReduction.whd ~subst context hetype) with 
                  Cic.Prod (n,s,t) ->
                    let arg,subst,metasenv,ugraph1 =
                      try