From 6c83c489af8968c4fcb942b518a9740dd870bddd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Jul 2019 18:21:18 +0200
Subject: [PATCH] Kill `bi_pow`.

---
 theories/examples/map.v       |  3 ++-
 theories/utils/contribution.v | 11 +++--------
 2 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/theories/examples/map.v b/theories/examples/map.v
index cdef133..e3362d5 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -126,7 +126,8 @@ Section map.
 
   Lemma par_map_workers_spec γl γ n vmap lk c :
     map_spec vmap -∗
-    {{{ is_lock N γl lk (map_worker_lock_inv γ c) ∗ client γ (∅:gmultiset A) ^ n }}}
+    {{{ is_lock N γl lk (map_worker_lock_inv γ c) ∗
+        [∗] replicate n (client γ (∅:gmultiset A)) }}}
       par_map_workers #n vmap lk c
     {{{ RET #(); True }}}.
   Proof.
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 1cdb68e..daffe13 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -20,12 +20,6 @@ Definition client `{contributionG Σ A} (γ : gname) (x : A) : iProp Σ :=
 Typeclasses Opaque client.
 Instance: Params (@client) 5.
 
-(** MOVE *)
-Fixpoint bi_pow {PROP : bi} (n : nat) (P : PROP) : PROP :=
-  match n with O => emp | S n => P ∗ bi_pow n P end%I.
-Arguments bi_pow {_} _ _%I.
-Notation "P ^ n" := (bi_pow n P) : bi_scope.
-
 Section contribution.
   Context `{contributionG Σ A}.
   Implicit Types x y : A.
@@ -140,10 +134,11 @@ Section contribution.
   Qed.
 
   (** Derived *)
-  Lemma contribution_init_pow n : (|==> ∃ γ, server γ n ε ∗ (client γ ε)^n)%I.
+  Lemma contribution_init_pow n :
+    (|==> ∃ γ, server γ n ε ∗ [∗] replicate n (client γ ε))%I.
   Proof.
     iMod (contribution_init) as (γ) "Hs". iExists γ.
-    iInduction n as [|n] "IH"; first by iFrame.
+    iInduction n as [|n] "IH"; simpl; first by iFrame.
     iMod ("IH" with "Hs") as "[Hs $]". by iApply alloc_client.
   Qed.
 End contribution.
-- 
GitLab