Incredible bug fixed: coercions were computed and then partially thrown away

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e4532d913bf77d69027eda8420bb9e65cdd1c7ca..09265ef2e4c265007218bb81382aba337deb0ff0 100644 (file)
--- 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