From c45a4837a6f3c9d6af14b2057389442bf6d2f32f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Oct 2008 22:24:01 +0000 Subject: [PATCH] subst_meta was missing --- helm/software/components/ng_refiner/nCicUnification.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 10bc29a62..24ab7b4af 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -174,6 +174,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap = try let _, _,oldt,_ = NCicUtils.lookup_subst n subst in let oldt = NCicSubstitution.subst_meta lc oldt in + let t = NCicSubstitution.subst_meta lc t in (* conjecture: always fail --> occur check *) unify test_eq_only metasenv subst context oldt t with NCicUtils.Subst_not_found _ -> @@ -181,7 +182,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap = * we could ? := Type_j with j <= i... *) let subst = (n, (name, ctx, t, ty)) :: subst in pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm - ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t))); + ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t))); let metasenv = List.filter (fun (m,_) -> not (n = m)) metasenv in -- 2.39.2