some fixed done in Orsay:

[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 e99ce5cd70285fe94680b80fdab6a20442b860c7..90643164d576bf14b5f309fc4011104bfa1d8b1b 100644 (file)
--- 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