From 24787f3d652537ec233f78bfa41a9230e7fa2f85 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 May 2008 13:23:50 +0000 Subject: [PATCH] meta VS meta in alpha_eq honors substitution --- helm/software/components/ng_kernel/nCicReduction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 9e43d0e24..47c8ea74d 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -512,7 +512,7 @@ let are_convertible whd ?(subst=[]) = | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2))) when n1 = n2 && s1 = s2 -> true - | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 -> + | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 && let l1 = NCicUtils.expand_local_context l1 in let l2 = NCicUtils.expand_local_context l2 in (try List.for_all2 @@ -520,7 +520,7 @@ let are_convertible whd ?(subst=[]) = (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)) l1 l2 - with Invalid_argument _ -> assert false) + with Invalid_argument _ -> assert false) -> true | C.Meta (n1,l1), _ -> (try -- 2.39.2