From 88a0b266486e0e6d2f8263a1cd643ba235442959 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 15 May 2009 21:14:15 +0000 Subject: [PATCH] added patch to not unify any term containing the in_scope tag with an entry in the local context --- .../components/ng_refiner/nCicMetaSubst.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 94cfe6690..432f3e4bf 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -220,6 +220,8 @@ let int_of_out_scope_tag tag = ;; +exception Found;; + (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), otherwise the occur check does not make sense in case of unification of ?n with ?n *) @@ -232,11 +234,22 @@ let delift ~unify metasenv subst context n l t = with NCicUtils.Subst_not_found _ -> false) | _ -> false in + let contains_in_scope subst t = + let rec aux _ () = function + | NCic.Meta _ as t -> + if is_in_scope_meta subst t then raise Found + else () + | t -> + if is_in_scope_meta subst t then raise Found + else NCicUtils.fold (fun _ () -> ()) () aux () t + in + try aux () () t; false with Found -> true + in let unify_list in_scope = match l with | _, NCic.Irl _ -> fun _ _ _ _ _ -> None | shift, NCic.Ctx l -> fun metasenv subst context k t -> - if flexible_arg subst t || is_in_scope_meta subst t then None else + if flexible_arg subst t || contains_in_scope subst t then None else let lb = List.map (fun t -> t, flexible_arg subst t) l in HExtlib.list_findopt (fun (li,flexible) i -> -- 2.39.2