From e305a62a7cb0a49fea3d241474e4c5bcd40e7272 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 27 Jan 2012 14:31:20 +0000 Subject: [PATCH] Fixes a bug in is_flexible (when checking a meta in subst, we did a recursive call on its body without applying the local context, resulting in various assertion failures). --- matita/components/ng_refiner/nCicMetaSubst.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml index f1fa293b3..57f12a458 100644 --- a/matita/components/ng_refiner/nCicMetaSubst.ml +++ b/matita/components/ng_refiner/nCicMetaSubst.ml @@ -260,18 +260,20 @@ and restrict status metasenv subst i (restrictions as orig) = ;; let rec is_flexible status context ~subst = function - | NCic.Meta (i,_) -> + | NCic.Meta (i,lc) -> + (try + let _,_,t,_ = NCicUtils.lookup_subst i subst in + let t = NCicSubstitution.subst_meta status lc t in + is_flexible status context ~subst t + with NCicUtils.Subst_not_found _ -> true) + | NCic.Appl (NCic.Meta (i,lc) :: args)-> (try - let _,_,t,_ = List.assoc i subst in - is_flexible status context ~subst t - with Not_found -> true) - | NCic.Appl (NCic.Meta (i,_) :: args)-> - (try - let _,_,t,_ = List.assoc i subst in + let _,_,t,_ = NCicUtils.lookup_subst i subst in + let t = NCicSubstitution.subst_meta status lc t in is_flexible status context ~subst (NCicReduction.head_beta_reduce status ~delta:max_int (NCic.Appl (t :: args))) - with Not_found -> true) + with NCicUtils.Subst_not_found _ -> true) (* this is a cheap whd, it only performs zeta-reduction. * * it works when the **omissis** disambiguation algorithm -- 2.39.2