From ca7c474381445e17d15ced6bf42da16946335598 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Nov 2005 15:59:38 +0000
Subject: [PATCH] Incredible bug fixed: coercions were computed and then
partially thrown away during eat_prods!
---
helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma | 3 +--
helm/ocaml/cic_unification/cicRefine.ml | 3 +--
2 files changed, 2 insertions(+), 4 deletions(-)
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
--
2.39.2