From 57307ff24cc63c11e70cf73c8bce96ce2d91cabd Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Thu, 28 May 2026 17:10:11 +0200 Subject: [PATCH 1/2] reexport expr equality and use same dummy on both sides --- src/ecReduction.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ecReduction.ml b/src/ecReduction.ml index d28cb2058..e268dab4e 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -185,7 +185,7 @@ module EqMod_base(Fe : sig val for_expr : env -> norm:bool -> (ident * ty) Mid.t -> expr -> expr -> bool end) = struct open EqTest_base - open Fe + include Fe (* ------------------------------------------------------------------ *) let rec for_stmt env alpha ~norm s1 s2 = @@ -1866,8 +1866,9 @@ module EqTest = struct include EqMod_base(struct let for_expr env ~norm:_ alpha e1 e2 = + let dummy_mem = EcIdent.create "&dummy" in let convert e = - let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in + let f = (ss_inv_of_expr dummy_mem e).inv in if Mid.is_empty alpha then f else From c243ba041b30ba2c40e11a077f5f19b3640b012b Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Thu, 7 May 2026 15:35:16 +0200 Subject: [PATCH 2/2] fall back to checking equality of expressions in `sim` Co-authored-by: Copilot --- src/ecPV.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/ecPV.ml b/src/ecPV.ml index 3d173b9b6..d25f946a3 100644 --- a/src/ecPV.ml +++ b/src/ecPV.ml @@ -1127,6 +1127,11 @@ module Mpv2 = struct when EcReduction.EqTest.for_type env ty1 ty2 && EcReduction.EqTest.for_type env b1.e_ty b2.e_ty -> List.fold_left2 (add_eqs_loc env local) eqs (b1::es1) (b2::es2) + | _, _ when EcReduction.EqTest.for_expr env e1 e2 -> + let fv1 = e_read env e1 in + let fv2 = e_read env e2 in + union eqs (eq_refl (PV.union fv1 fv2)) + | _, _ -> raise EqObsInError let add_eqs env e1 e2 eqs = add_eqs_loc env Mid.empty eqs e1 e2