From 725d4329707163927bb5cee3c2ccbdc8f1ab2967 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 May 2020 18:48:16 +0200
Subject: [PATCH] Rename `inv_sep` into `env_split`.

---
 theories/base_logic/lib/invariants.v | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index a1af8026d..25bf0a9a6 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -165,22 +165,20 @@ Section inv.
     iIntros "!> {$HP} HP". iApply "Hclose"; auto.
   Qed.
 
-  Lemma inv_sep_l N P Q : inv N (P ∗ Q) -∗ inv N P.
+  Lemma inv_split_l N P Q : inv N (P ∗ Q) -∗ inv N P.
   Proof.
     iIntros "#HI". iApply inv_alter; eauto.
     iIntros "!> !> [$ $] $".
   Qed.
-
-  Lemma inv_sep_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
+  Lemma inv_split_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
   Proof.
-    rewrite (comm _ P Q). eapply inv_sep_l.
+    rewrite (comm _ P Q). eapply inv_split_l.
   Qed.
-
-  Lemma inv_sep N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
+  Lemma inv_split N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
   Proof.
     iIntros "#H".
-    iPoseProof (inv_sep_l with "H") as "$".
-    iPoseProof (inv_sep_r with "H") as "$".
+    iPoseProof (inv_split_l with "H") as "$".
+    iPoseProof (inv_split_r with "H") as "$".
   Qed.
 
 End inv.
-- 
GitLab