From 58b72e344aa92542e326788bd426f1141fe09058 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 May 2021 12:36:39 +0200
Subject: [PATCH] =?UTF-8?q?rename=20big=5FsepL=5FsepL2=20=E2=86=92=20big?=
 =?UTF-8?q?=5FsepL2=5FsepL=20(and=20similar=20for=20sepM)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/bi/big_op.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index e7b702f29..8f29847b1 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -743,19 +743,19 @@ Section sep_list2.
     by rewrite IH.
   Qed.
 
-  Lemma big_sepL_sepL2 (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
+  Lemma big_sepL2_sepL (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
     length l1 = length l2 →
     ([∗ list] k↦y1;y2 ∈ l1;l2, Φ1 k y1 ∗ Φ2 k y2) ⊣⊢
     ([∗ list] k↦y1 ∈ l1, Φ1 k y1) ∗ ([∗ list] k↦y2 ∈ l2, Φ2 k y2).
   Proof.
     intros. rewrite -big_sepL_sep_zip // big_sepL2_alt pure_True // left_id //.
   Qed.
-  Lemma big_sepL_sepL2_2 (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
+  Lemma big_sepL2_sepL_2 (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
     length l1 = length l2 →
     ([∗ list] k↦y1 ∈ l1, Φ1 k y1) -∗
     ([∗ list] k↦y2 ∈ l2, Φ2 k y2) -∗
     [∗ list] k↦y1;y2 ∈ l1;l2, Φ1 k y1 ∗ Φ2 k y2.
-  Proof. intros. apply wand_intro_r. by rewrite big_sepL_sepL2. Qed.
+  Proof. intros. apply wand_intro_r. by rewrite big_sepL2_sepL. Qed.
 
   Global Instance big_sepL2_nil_persistent Φ :
     Persistent ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
@@ -1715,19 +1715,19 @@ Section map2.
     apply big_sepM2_mono. eauto.
   Qed.
 
-  Lemma big_sepM_sepM2 (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
+  Lemma big_sepM2_sepM (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
     (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ1 k y1 ∗ Φ2 k y2) ⊣⊢
     ([∗ map] k↦y1 ∈ m1, Φ1 k y1) ∗ ([∗ map] k↦y2 ∈ m2, Φ2 k y2).
   Proof.
     intros. rewrite -big_sepM_sep_zip // big_sepM2_alt pure_True // left_id //.
   Qed.
-  Lemma big_sepM_sepM2_2 (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
+  Lemma big_sepM2_sepM_2 (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
     (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
     ([∗ map] k↦y1 ∈ m1, Φ1 k y1) -∗
     ([∗ map] k↦y2 ∈ m2, Φ2 k y2) -∗
     [∗ map] k↦y1;y2 ∈ m1;m2, Φ1 k y1 ∗ Φ2 k y2.
-  Proof. intros. apply wand_intro_r. by rewrite big_sepM_sepM2. Qed.
+  Proof. intros. apply wand_intro_r. by rewrite big_sepM2_sepM. Qed.
 
   Global Instance big_sepM2_empty_persistent Φ :
     Persistent ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
-- 
GitLab