From f094694e53cfeea2c33e8c2aa2abac6dd7e44138 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Apr 2009 13:09:16 +0000 Subject: [PATCH] =?utf8?q?=3F=5FOS1=20:=3D=20C[=20=3F=5FIN=20]=20=3F=5FIN?= =?utf8?q?=20:=3D=20m=20=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D?= =?utf8?q?=3D=3D=3D=3D=3D=3D=3D=20=3F[m;m]=20=20=3D=3F=3D=20=20=3F=5FOS1?= used to yield ? := Rel 2 instead of Rel 1, since the first m was still out of scope when recursion reaches ?_IN --- helm/software/components/ng_refiner/nCicMetaSubst.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index adc1ac620..94cfe6690 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -224,11 +224,19 @@ let int_of_out_scope_tag tag = otherwise the occur check does not make sense in case of unification of ?n with ?n *) let delift ~unify metasenv subst context n l t = + let is_in_scope_meta subst = function + | NCic.Meta (i,_) -> + (try + let tag, _, _, _ = NCicUtils.lookup_subst i subst in + tag = Some in_scope_tag + with NCicUtils.Subst_not_found _ -> false) + | _ -> false + 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 then None else + if flexible_arg subst t || is_in_scope_meta 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