From db3c672de3bea4ec2973e68118c7e02fbf685bba Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 12 Jun 2020 10:58:34 +0200
Subject: [PATCH] refines_exists -> refines_pack

---
 theories/examples/bit.v                   | 2 +-
 theories/examples/cell.v                  | 2 +-
 theories/examples/namegen.v               | 2 +-
 theories/examples/stack/refinement.v      | 2 +-
 theories/examples/symbol.v                | 4 ++--
 theories/examples/ticket_lock.v           | 2 +-
 theories/experimental/hocap/ticket_lock.v | 2 +-
 theories/logic/compatibility.v            | 2 +-
 8 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index 50fce0a..c677894 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -26,7 +26,7 @@ Section bit_refinement.
   Lemma bit_refinement Δ : ⊢ REL bit_bool << bit_nat : interp bitτ Δ.
   Proof.
     unfold bitτ; simpl.
-    iApply (refines_exists R).
+    iApply (refines_pack R).
     progress repeat iApply refines_pair.
     - rel_values.
     - unfold flip_nat. rel_pure_l.
diff --git a/theories/examples/cell.v b/theories/examples/cell.v
index bbdbc55..97d00a9 100644
--- a/theories/examples/cell.v
+++ b/theories/examples/cell.v
@@ -58,7 +58,7 @@ Section cell_refinement.
   Proof.
     unfold cell1, cell2.
     iApply refines_forall. iIntros "!#" (R).
-    iApply (refines_exists (cellR R)).
+    iApply (refines_pack (cellR R)).
     repeat iApply refines_pair.
     - (* New cell *)
       rel_pure_l. rel_pure_r.
diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index 2f86e68..3dfe5cf 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -47,7 +47,7 @@ Section namegen_refinement.
     iMod (inv_alloc N _ (ng_Inv γ c) with "[-]") as "#Hinv".
     { iNext. iExists 0, ∅. iFrame.
       by rewrite big_sepS_empty. }
-    iApply (refines_exists (ngR γ)).
+    iApply (refines_pack (ngR γ)).
     do 2 rel_pure_r.
     iApply refines_pair.
     - (* New name *)
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index c810915..c2984a5 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -169,7 +169,7 @@ Section proof.
   Proof.
     unfold CG_stack, FG_stack.
     iApply refines_forall. iIntros (A). iAlways.
-    iApply (refines_exists (stackInt A)).
+    iApply (refines_pack (stackInt A)).
     repeat iApply refines_pair.
     - unfold CG_new_stack, FG_new_stack.
       iApply refines_arrow_val. iAlways.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index d5eace0..3a534e2 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -235,7 +235,7 @@ Section proof.
     rel_apply_l (refines_newlock_l N (lok_inv size1 size2 tbl1 tbl2 l2)%I with "[Hs1' Hs2' Htbl1' Htbl2' Hl2]").
     { iExists 0,_. by iFrame. }
     iNext. iIntros (l1 γl) "#Hl1". rel_pure_l. rel_pure_l.
-    iApply (refines_exists (tableR γ)).
+    iApply (refines_pack (tableR γ)).
     repeat iApply refines_pair.
     (* Eq *)
     - iApply eqKey_refinement.
@@ -314,7 +314,7 @@ Section proof.
     rel_apply_l (refines_newlock_l N (lok_inv size1 size2 tbl1 tbl2 l2)%I with "[Hs1' Hs2' Htbl1' Htbl2' Hl2]").
     { iExists 0,_. by iFrame. }
     iNext. iIntros (l1 γl) "#Hl1". rel_pure_l. rel_pure_l.
-    iApply (refines_exists (tableR γ)).
+    iApply (refines_pack (tableR γ)).
     repeat iApply refines_pair.
     (* Eq *)
     - iApply eqKey_refinement.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index d3eef81..4d82bdc 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -346,7 +346,7 @@ Section refinement.
         (reloc.lib.lock.newlock, reloc.lib.lock.acquire, reloc.lib.lock.release)
     : lrel_lock.
   Proof.
-    simpl. iApply (refines_exists lockInt).
+    simpl. iApply (refines_pack lockInt).
     repeat iApply refines_pair.
     - by iApply newlock_refinement.
     - by iApply acquire_refinement_direct.
diff --git a/theories/experimental/hocap/ticket_lock.v b/theories/experimental/hocap/ticket_lock.v
index 2aa85b9..d0f33f9 100644
--- a/theories/experimental/hocap/ticket_lock.v
+++ b/theories/experimental/hocap/ticket_lock.v
@@ -126,7 +126,7 @@ Section refinement.
             <<
            (spin_lock.newlock, spin_lock.acquire, spin_lock.release) : interp lockT Δ.
   Proof.
-    iApply (refines_exists lockInt).
+    iApply (refines_pack lockInt).
     repeat iApply refines_pair; simpl.
     - by iApply newlock_refinement.
     - by iApply acquire_refinement.
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 73c57a5..2cb61fb 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -68,7 +68,7 @@ Section compatibility.
     - iExists #(); eauto.
   Qed.
 
-  Lemma refines_exists (A : lrel Σ) e e' (C : lrel Σ → lrel Σ) :
+  Lemma refines_pack (A : lrel Σ) e e' (C : lrel Σ → lrel Σ) :
     (REL e << e' : C A) -∗
     REL e << e' : ∃ A, C A.
   Proof.
-- 
GitLab