From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Nov 2005 15:59:38 +0000 (+0000)
Subject: Incredible bug fixed: coercions were computed and then partially thrown away
X-Git-Tag: V_0_7_2_3~39
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ca7c474381445e17d15ced6bf42da16946335598

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 0fd993411..3e59a68d1 100644
--- 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 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