refines_exists -> refines_pack

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.

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.

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 *)

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.

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.

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.

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.

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.