From ca7c474381445e17d15ced6bf42da16946335598 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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.5