fix bug in conv of equivS

EasyCrypt · Dec 7, 2023 · a8e6929 · a8e6929
1 parent 4ff34a2
commit a8e6929
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
@@ -1719,7 +1719,7 @@ let rec conv ri env f1 f2 stk =
   | FequivS es1, FequivS es2
       when EqTest_i.for_stmt env es1.es_sl es2.es_sl
         && EqTest_i.for_stmt env es1.es_sr es2.es_sr ->
-    begin match check_me_bindings env EcSubst.empty [es1.es_ml; es1.es_ml] [es2.es_ml; es2.es_mr] with
+    begin match check_me_bindings env EcSubst.empty [es1.es_ml; es1.es_mr] [es2.es_ml; es2.es_mr] with
     | subst ->
       let subst = EcSubst.subst_form subst in
       conv ri env es1.es_pr (subst es2.es_pr) (zhl f1 [es1.es_po] [subst es2.es_po] stk)