X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=09265ef2e4c265007218bb81382aba337deb0ff0;hb=ca7c474381445e17d15ced6bf42da16946335598;hp=e4532d913bf77d69027eda8420bb9e65cdd1c7ca;hpb=f5708603f309bf12ac31c15ebedfdaf8e879283e;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e4532d913..09265ef2e 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1102,8 +1102,7 @@ and type_of_aux' metasenv context t ugraph =
                    in
                    let coerced_args,metasenv',subst',t',ugraph2 =
                      eat_prods metasenv subst context
-                       (* (CicMetaSubst.subst subst hete t) tl *)
-                       (CicSubstitution.subst hete t) ugraph1 tl
+                      (CicSubstitution.subst arg t) ugraph1 tl
                    in
                      arg::coerced_args,metasenv',subst',t',ugraph2
                | _ -> assert false