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

during eat_prods!

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
index 0fd99341142e450e3221635223cd126b60ce0cf4..3e59a68d18eb997cce5e3354855833a3b774831f 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
@@ -24,7 +24,6 @@ record QD: Type \def {
 }.
 
 coercion qd.
-(*
+
 inductive iall (D:QD) (P:D \to Prop) : Prop \def
    | iall_intro: (\forall (a:D). acin D a \to P a) \to iall D P.
-*)   

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