From 19b5051af1cb82b8108b66622b6391291112929e Mon Sep 17 00:00:00 2001
From: Dmitry Khalanskiy <Dmitry.Khalanskiy@jetbrains.com>
Date: Thu, 23 Jan 2020 10:00:19 +0300
Subject: [PATCH] Rename parameters in  due to conventions

---
 theories/algebra/cmra.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 8a409fdbf..487ec1e32 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1204,7 +1204,7 @@ Section prod_unit.
   Qed.
   Canonical Structure prodUR := UcmraT (prod A B) prod_ucmra_mixin.
 
-  Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ε) ⋅ (ε, y).
+  Lemma pair_split (a : A) (b : B) : (a, b) ≡ (a, ε) ⋅ (ε, b).
   Proof. by rewrite -pair_op left_id right_id. Qed.
 
   Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
-- 
GitLab