From 8057bfa1cbd381801dc10dbea805b34ecfc3b770 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Thu, 7 May 2026 14:22:24 +0200 Subject: [PATCH] Check equality of expressions up to convertibility Co-authored-by: Copilot --- src/ecReduction.ml | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/src/ecReduction.ml b/src/ecReduction.ml index d28cb2058..cb11a76ef 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -1864,26 +1864,28 @@ let hs_inv_alpha_eq hyps (inv1 : hs_inv) (inv2 : hs_inv) = module EqTest = struct include EqTest_base - include EqMod_base(struct - let for_expr env ~norm:_ alpha e1 e2 = - let convert e = - let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in + let for_expr env ~norm:_ alpha e1 e2 = + let convert e = + let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in + + if Mid.is_empty alpha then f else - if Mid.is_empty alpha then f else + let subst = + Mid.fold + (fun x (y, ty) subst -> + Fsubst.f_bind_local subst x (f_local y ty)) + alpha Fsubst.f_subst_id - let subst = - Mid.fold - (fun x (y, ty) subst -> - Fsubst.f_bind_local subst x (f_local y ty)) - alpha Fsubst.f_subst_id + in Fsubst.f_subst subst f in - in Fsubst.f_subst subst f in + let f1 = convert e1 in + let f2 = convert e2 in - let f1 = convert e1 in - let f2 = convert e2 in + is_conv (LDecl.init env []) f1 f2 - is_conv (LDecl.init env []) f1 f2 - end) + include EqMod_base(struct + let for_expr = for_expr + end) let for_pv = fun env ?(norm = true) -> for_pv env ~norm let for_lv = fun env ?(norm = true) -> for_lv env ~norm