From 162c5c145ea1a9e8ee5948fefeb716bad02a99db Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 14 Oct 2025 17:50:55 +0200 Subject: [PATCH 1/2] fix printing logic for synchronized equivs --- src/ecReduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ecReduction.ml b/src/ecReduction.ml index 40fb0ec84..1dce11fab 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -1825,7 +1825,7 @@ module EqTest = struct include EqMod_base(struct let for_expr env ~norm:_ alpha e1 e2 = let convert e = - let f = form_of_expr e in + let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in if Mid.is_empty alpha then f else From 4ecc52f4213a64fede75c21ad993e6cfa6af2f75 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 14 Oct 2025 17:54:31 +0200 Subject: [PATCH 2/2] fix `byequiv` with trivial precondition --- src/phl/ecPhlDeno.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/phl/ecPhlDeno.ml b/src/phl/ecPhlDeno.ml index e89fc1360..0a6ce9af2 100644 --- a/src/phl/ecPhlDeno.ml +++ b/src/phl/ecPhlDeno.ml @@ -436,7 +436,7 @@ let process_pre tc hyps prl prr pre post = let gen_r f = ss_inv_generalize_right f mr in let gen_l f = ss_inv_generalize_left f ml in dof fl al ml pml gen_r; dof fr ar mr pmr gen_l; - map_ts_inv f_ands !eqs + map_ts_inv ~ml ~mr f_ands !eqs (* -------------------------------------------------------------------- *) let post_iff ml mr eq env evl evr =