From d3ee3b1173e880b33f064551654c96ab4c292363 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Oct 2009 09:49:13 +0000 Subject: [PATCH] instantiate merges tags --- .../components/ng_refiner/nCicUnification.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index d48dfaf46..5669b1abc 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -328,6 +328,21 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = (* conjecture: always fail --> occur check *) unify test_eq_only metasenv subst context oldt t with NCicUtils.Subst_not_found _ -> + let metasenv, tags = + let rec aux = function + | NCic.Meta (j,lc) -> + (try + let _, _, t, _ = NCicUtils.lookup_subst j subst in + aux (NCicSubstitution.subst_meta lc t) + with NCicUtils.Subst_not_found _ -> + let tags', ctx, ty = NCicUtils.lookup_meta j metasenv in + let metasenv = List.remove_assoc j metasenv in + let tags = tags @ tags' in + (j, (tags, ctx, ty)) :: metasenv, tags) + | _ -> metasenv, tags + in + aux t + in (* by cumulativity when unify(?,Type_i) * we could ? := Type_j with j <= i... *) let subst = (n, (tags, ctx, t, ty)) :: subst in -- 2.39.2