diff --git a/opam b/opam
index 437cfece431be49c0c6103c32cba4b64dba1ac0f..f88680d1cb7b4c08185dbd2de22f724a18268232 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-03-03.3") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-03-04.7") | (= "dev") }
 ]
diff --git a/theories/escrows.v b/theories/escrows.v
index 3b6de32f8c907e57e2d5541afada5c9be7815b84..3bf228337c2a82e655477424ed6f33e1bbda20f7 100644
--- a/theories/escrows.v
+++ b/theories/escrows.v
@@ -30,7 +30,7 @@ Section Escrows.
   Proof. solve_contractive. Qed.
 
   Definition escrow P Q : vProp Σ :=
-    (∃ β, exchange (∃ᵢ P) Q β)%I.
+    (∃ β, exchange (<subj> P) Q β)%I.
 
   Global Instance escrow_proper : Proper ((≡) ==> (≡) ==> (≡)) escrow.
   Proof. intros ?? H ?? H2. apply: bi.exist_proper => ?. by rewrite H H2. Qed.
@@ -124,13 +124,13 @@ Section proof.
   Proof. by apply exchange_alloc_r. Qed.
 
   Lemma escrow_apply_obj P Q:
-    (P ∗ P → False) ⊢ ([es P ⇝ Q] ∗ ▷ ∃ᵢ P ={↑escrowN}=∗ ▷ Q).
+    (P ∗ P → False) ⊢ ([es P ⇝ Q] ∗ ▷ <subj> P ={↑escrowN}=∗ ▷ Q).
   Proof.
     iStartProof (uPred _). iIntros (V0) "ND".
     rewrite /escrow /exchange /=. iIntros (V ?) "(Esc & oP)".
     iDestruct "Esc" as (V') "[% ?]".
     iInv escrowN as "Inv" "HClose".
-    iAssert (▷ (Q V' ∗ ((∃ᵢ P)%I V' ∨ Q V')))%I with "[ND oP Inv]" as "[Q Inv]".
+    iAssert (▷ (Q V' ∗ ((<subj> P)%I V' ∨ Q V')))%I with "[ND oP Inv]" as "[Q Inv]".
       { iNext. iDestruct "Inv" as "[Inv|$]".
         - iExFalso.
           iDestruct "oP" as (V1) "P1".
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index 6d2b96b1ad6a5862e3352e0c6c480875ec07ea15..a6381fd865e565666dd73652d0c24e8c13148be3 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -286,7 +286,7 @@ Section CircBuffer.
       wp_lam. wp_bind ([_]_at)%E. wp_op.
 
       iApply (GPS_SW_Read_ex with "[$kI $pW]"); [done|done|..].
-      { rewrite monPred_absolutely_unfold. iIntros (????) "!> #$ //". }
+      { rewrite monPred_objectively_unfold. iIntros (????) "!> #$ //". }
 
       iNext. iIntros (w) "(pW & #CEs)".
       iDestruct "CEs" as "(% & CEs)".
@@ -298,7 +298,7 @@ Section CircBuffer.
                 with "[$kI $cR]"); [done|done|..].
       { iSplitL.
         - iIntros (?). iIntros "_". iLeft. by iIntros "!>" (?) "(? & _)".
-        - rewrite monPred_absolutely_unfold. iIntros "!>" (?????) "[? #$] //". }
+        - rewrite monPred_objectively_unfold. iIntros "!>" (?????) "[? #$] //". }
 
       iNext. iIntros (j r) "(% & #cR2 & #PEs)".
       iDestruct "PEs" as "(% & PEs)".
@@ -390,7 +390,7 @@ Section CircBuffer.
                 with "[$kI $pR]"); [done|done|..].
       { iSplitL.
         - iIntros (??). iLeft. iIntros "!>" (?) "(? & _)". by auto.
-        - rewrite monPred_absolutely_unfold. iIntros "!>" (?????) "[? #$] //". }
+        - rewrite monPred_objectively_unfold. iIntros "!>" (?????) "[? #$] //". }
 
       iNext. iIntros (i w) "(% & pR & #CEs)".
       iDestruct "CEs" as "(% & CEs)".
@@ -399,7 +399,7 @@ Section CircBuffer.
 
       iApply (GPS_SW_Read_ex
                 with "[$kI $cW]"); [done|done|..].
-      { rewrite monPred_absolutely_unfold. iIntros "!>" (????) "!> #$ //". }
+      { rewrite monPred_objectively_unfold. iIntros "!>" (????) "!> #$ //". }
 
       iNext. iIntros (r) "(cW & #PEs)".
       iDestruct "PEs" as "(% & PEs)".
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index c3e4fa93f5bb59860082640c1e8ca70429e24cb3..3f3137b6b8712a0a60308503c3efebc4f79d4195 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -601,7 +601,7 @@ Section proof.
           iFrame.
           iApply ("HP" with "HH").
       - iSplit; [|iSplit; auto].
-        iNext; iApply absolute_absolutely.
+        iNext; iApply objective_objectively.
         iIntros (? ?) "[? #?]"; iModIntro; iFrame "#". }
     iNext. iIntros (s' k') "(% & #Hk' & % & Hpost)"; subst.
     iMod "Hpost"; iModIntro.
@@ -670,7 +670,7 @@ Section proof.
             eapply Hzero; auto.
             eapply lookup_weaken; eauto.
         + iSplit; last auto.
-          iNext; iApply absolute_absolutely.
+          iNext; iApply objective_objectively.
           iIntros (? ?) "[? #?]"; iModIntro; iFrame "#". }
       iNext. iIntros (s' v) "[% ?]"; auto.
     - rewrite bool_decide_false; last done.
@@ -960,7 +960,7 @@ Section proof.
           iFrame.
           by iMod ("HP" with "HH"); iFrame.
       - iSplit; [|iSplit; auto].
-        iNext; iApply absolute_absolutely.
+        iNext; iApply objective_objectively.
         iIntros (? ?) "[? #?]"; iModIntro; iFrame "#". }
     iNext. iIntros (s' k') "(% & % & Hpost)"; subst.
     iMod "Hpost"; iModIntro.
@@ -1062,7 +1062,7 @@ Section proof.
           iMod "Hsnap'" as "[% ?]"; subst.
           iModIntro; iSplit; [done | iFrame].
           iApply "HP"; iFrame; iSplit; done.
-        + iNext; iApply absolute_absolutely.
+        + iNext; iApply objective_objectively.
           iIntros (? ?) "[? #?]"; iModIntro; iFrame "#".
         + iFrame; done. }
       iNext. iIntros (? b k') "(% & Hpost)".
@@ -1119,7 +1119,7 @@ Section proof.
             + iPoseProof (and_elim_l with "Hrest") as "HP".
               by iMod ("HP" with "HH"); iFrame.
           - iSplit; [|iSplit; auto].
-            iNext; iApply absolute_absolutely.
+            iNext; iApply objective_objectively.
             iIntros (? ?) "[? #?]"; iModIntro; iFrame "#". }
         iNext. iIntros (? k'') "(% & % & Hsnap & Hpost)"; subst.
         destruct H5; try contradiction; subst k''.
@@ -1378,7 +1378,7 @@ Section proof.
          iSplit; last by rewrite (nth_lookup_Some _ _ _ _ H0); auto.
          iPureIntro; do 2 eexists; eauto; done.
        + rewrite Hx; auto.
-     - iNext; iApply absolute_absolutely.
+     - iNext; iApply objective_objectively.
        iIntros (? ?) "[? #?]"; iModIntro; iFrame "#".
      - iFrame; done. }
     iNext. iIntros (? b ?) "[% Hpost]".
@@ -1781,15 +1781,15 @@ Section proof.
         try (apply Permutation_map; symmetry; eassumption); done.
   Qed.
 
-  Instance hashtable_inv_absolute : Absolute (hashtable_inv gh g lgk lgv H).
+  Instance hashtable_inv_objective : Objective (hashtable_inv gh g lgk lgv H).
   Proof.
     intros; unfold hashtable_inv.
-    apply sep_absolute, _.
+    apply sep_objective, _.
     unfold hashtable.
-    apply exists_absolute; intro.
-    apply sep_absolute; first apply _.
-    apply sep_absolute; first apply _.
-    apply big_sepL_absolute; intros ? (?, ?).
+    apply exists_objective; intro.
+    apply sep_objective; first apply _.
+    apply sep_objective; first apply _.
+    apply big_sepL_objective; intros ? (?, ?).
     apply _.
   Qed.
 
@@ -1871,12 +1871,12 @@ Section proof.
       iExists _; iSplit; first by iCombine "Hhist Ht" as "H"; iApply "H".
       iIntros "!# [>Hhist Ht]".
       iMod (inv_open with "Hinv") as "[>HH Hclose]"; first auto.
-      iDestruct (monPred_absolutely_elim with "HH") as (HT) "[HH H]".
+      iDestruct (monPred_objectively_elim with "HH") as (HT) "[HH H]".
       iModIntro; iExists HT; iFrame "HH".
       iSplit.
       { iIntros "HH".
         iMod ("Hclose" with "[HH H]"); last by iFrame.
-        iNext; iApply absolute_absolutely.
+        iNext; iApply objective_objectively.
         iExists HT; iFrame. }
       iDestruct "H" as (hr) "[% H]"; iDestruct "H" as (mr) "[% Hg]".
       iIntros (v) "H"; iDestruct "H" as (b lv) "(Hentries & H & % & HH)"; iDestruct "H" as (T) "[% HA']".
@@ -1897,7 +1897,7 @@ Section proof.
       destruct H5 as (? & Hb & Hadd); subst v.
       iMod ("Hclose" with "[HH Hg]").
       { iNext.
-        iApply absolute_absolutely.
+        iApply objective_objectively.
         iExists (if b then map_upd HT (i + 1) lv else HT); iFrame.
         iExists (hr ++ HAdd (i + 1) 1 b :: nil)%list; iSplit.
         { iPureIntro; rewrite apply_hist_app.
@@ -2043,7 +2043,7 @@ Section proof.
     set (N := namespaces.ndot namespaces.nroot "N").
     iMod (inv_alloc N top (∃H, hashtable_inv gh g lgk lgv H)%I with "[HH Href]") as "#Hinv".
     { iNext.
-      iApply absolute_absolutely.
+      iApply objective_objectively.
       iExists (λ _ : Z, None); iFrame.
       iExists nil; iSplit; first auto.
       iExists ∅; rewrite fmap_empty; auto. }
@@ -2177,8 +2177,8 @@ Section proof.
             do 2 apply namespaces.ndot_preserve_disjoint_r.
             apply namespaces.ndot_ne_disjoint; done. }
           iMod "H"; iModIntro; auto.
-        * iNext; do 2 (rewrite monPred_absolutely_forall; iIntros (?)).
-          iApply absolutely_entails.
+        * iNext; do 2 (rewrite monPred_objectively_forall; iIntros (?)).
+          iApply objectively_entails.
           iIntros "[? #?]"; iModIntro; iFrame "#". }
       iNext; iIntros (b ?) "(% & _ & % & Hcond)"; subst.
       iExists (Z.b2z b); iSplit; first auto.
@@ -2222,7 +2222,7 @@ Section proof.
     { apply namespaces.ndisj_subseteq_difference; last auto.
       apply namespaces.ndot_ne_disjoint; done. }
     iNext; iIntros (?) "[% Htotal]"; subst.
-    iDestruct (monPred_absolutely_elim with "Href") as (HT) "[HH Href]".
+    iDestruct (monPred_objectively_elim with "Href") as (HT) "[HH Href]".
     iDestruct "Href" as (hr) "[% Href]".
     iDestruct "Href" as (mr) "[% Href]".
     assert (i = 3) by omega; subst.
@@ -2235,7 +2235,7 @@ Section proof.
     replace (_ â‹… _) with 1%Qp.
     iPoseProof (own_valid_2 with "Href Hhist") as "%".
     iMod ("Hclose" with "[HH Href]").
-    { iNext; iApply absolute_absolutely.
+    { iNext; iApply objective_objectively.
       iExists HT; iFrame; auto. }
     iModIntro; iApply "Hpost".
     iPureIntro.
diff --git a/theories/examples/kvnode.v b/theories/examples/kvnode.v
index 1473982bf11570d0ab85c603a613cc255aede0dc..9f2aa9893b29434b2e0cb891dc785a86878f8b94 100644
--- a/theories/examples/kvnode.v
+++ b/theories/examples/kvnode.v
@@ -488,8 +488,8 @@ Section proof.
       iSplitR ""; [|iSplit].
       - iNext; iIntros (s Hs).
         by iLeft; iIntros (?) "[? _]".
-      - iNext; do 2 (rewrite monPred_absolutely_forall; iIntros (?)).
-        iApply absolutely_entails.
+      - iNext; do 2 (rewrite monPred_objectively_forall; iIntros (?)).
+        iApply objectively_entails.
         iIntros "[? #?]"; iModIntro; iFrame "#".
       - iSplit; first auto.
         by iDestruct "node_state" as "(? & ? & ?)". }
@@ -548,8 +548,8 @@ Section proof.
           destruct H1 as (_ & ? & ?).
           eapply log_latest_ord; eauto.
           apply fmap_nth_log_latest; eauto.
-        + iNext; do 2 (rewrite monPred_absolutely_forall; iIntros (?)).
-          iApply absolutely_entails.
+        + iNext; do 2 (rewrite monPred_objectively_forall; iIntros (?)).
+          iApply objectively_entails.
           iIntros "[? #?]"; iModIntro; iFrame "#". }
       iNext; iIntros (s d) "(% & Hdi & H)"; iDestruct "H" as (vi) "(% & #kV'')".
       iApply wp_fupd.
@@ -658,8 +658,8 @@ Section proof.
               specialize (X i); rewrite !lookup_fmap HL1 HL' in X; done.
           + eapply lookup_weaken; last eauto.
             destruct Hlatest; done.
-        - iNext; do 2 (rewrite monPred_absolutely_forall; iIntros (?)).
-          iApply absolutely_entails.
+        - iNext; do 2 (rewrite monPred_objectively_forall; iIntros (?)).
+          iApply objectively_entails.
           iIntros "[? #?]"; iModIntro; iFrame "#".
         - iSplit; first auto.
           by iDestruct "node_state" as "(? & ? & ?)". }
@@ -731,8 +731,8 @@ Section proof.
     iDestruct "node_state" as "(% & kV & oL & data)".
     iApply (GPS_SW_Read_ex (versionP n g) with "[$kI $kV]");
       [auto | auto | ..].
-    { iNext; rewrite monPred_absolutely_forall; iIntros (?).
-      iApply absolutely_entails.
+    { iNext; rewrite monPred_objectively_forall; iIntros (?).
+      iApply objectively_entails.
       iIntros "#?"; iModIntro; iFrame "#". }
     iNext; iIntros (?) "(kV & Hv)".
     rewrite versionP_eq.
diff --git a/theories/examples/message_passing.v b/theories/examples/message_passing.v
index e4d570bb91ee26ee205ef7ba1a4741824d68dcdf..e1a56e42e1afb06aa740edd079f37b77630bc964 100644
--- a/theories/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -96,7 +96,7 @@ Section proof.
       + iSplitL.
         * iNext. iIntros (?). iIntros "_".
           iLeft. iIntros (?) "[YP  _]". by simpl.
-        * rewrite monPred_absolutely_unfold /=. iIntros (?????) "!> [_ #$] //".
+        * rewrite monPred_objectively_unfold /=. iIntros (?????) "!> [_ #$] //".
       + iNext. iIntros (s v) "(_ & #yPRT5 & #YP)".
         destruct s.
         * iDestruct "YP" as "(% & XE)".
diff --git a/theories/examples/msqueue.v b/theories/examples/msqueue.v
index 4e0db8c90b2bdaf26d121434d820d16a1b77b577..460184cbdfd81238c35e81233a3e91f54178d965 100644
--- a/theories/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -230,7 +230,7 @@ Section MSQueue.
         [done|done|..].
       { iSplitL "".
         - iNext. iIntros ([] ?). iLeft. by iIntros (x) "($ & _)".
-        - rewrite monPred_absolutely_unfold /=. iIntros (?????) "!> [_ #$] //". }
+        - rewrite monPred_objectively_unfold /=. iIntros (?????) "!> [_ #$] //". }
       iNext. iIntros ([] x) "(_ & _ & % & ox)".
       wp_seq. wp_bind ([_]_at)%E. wp_op. wp_op.
       rewrite (_ : ZplusPos 0 (Z.to_pos x) = Z.to_pos (x + 0)); last first.
@@ -250,7 +250,7 @@ Section MSQueue.
             iDestruct "LinkInt" as (γ') "(_ & Link)".
             iSplitL ""; first (iPureIntro; lia).
             iExists γ'. subst v. iFrame "Link".
-        - rewrite monPred_absolutely_unfold /=. iIntros (????) "!> _ (_ & #$) //". }
+        - rewrite monPred_objectively_unfold /=. iIntros (????) "!> _ (_ & #$) //". }
 
       iNext. iIntros (s n') "(% & _ & Q)".
       wp_seq. wp_op; case_bool_decide.
@@ -324,7 +324,7 @@ Section MSQueue.
                   with "kI [P Tok od Link]");
           [done|done|..].
         { iFrame "Tok Link". iSplitR "P od"; last iSplitR "P od"; last first.
-          - rewrite monPred_absolutely_unfold /=.
+          - rewrite monPred_objectively_unfold /=.
             iIntros "{$P $od}" (????) "!> _ (_ & #$) //".
           - iNext. iIntros (??) "(_ & _ & _ & ? & ? & _)". by iFrame.
           - iNext. iIntros (s'). iIntros "(_ & LinkInt & P')".
@@ -375,7 +375,7 @@ Section MSQueue.
         [done|done|..].
       { iSplitL.
         - iIntros ([]) "_". iLeft. by iIntros "!>" (x) "($ & _)".
-        - rewrite monPred_absolutely_unfold /=. iIntros "!>" (????) "_ (_ & #$) //". }
+        - rewrite monPred_objectively_unfold /=. iIntros "!>" (????) "_ (_ & #$) //". }
 
       iNext. iIntros ([] s) "(_ & oH2 & % & os)".
       iDestruct "os" as (γ) "os".
@@ -406,7 +406,7 @@ Section MSQueue.
             rewrite (_: Z.to_pos (Z.pos l' + 1) = ZplusPos 1 l'); last first.
             { rewrite /ZplusPos. f_equal. omega. }
             iFrame "DEQ Link".
-        - rewrite monPred_absolutely_unfold /=. iIntros "!>" (????) "_ [_ #$] //". }
+        - rewrite monPred_objectively_unfold /=. iIntros "!>" (????) "_ [_ #$] //". }
 
       iNext. iIntros (s' n) "(_ & #os & Q')".
       wp_seq. wp_op. case_bool_decide.
@@ -421,7 +421,7 @@ Section MSQueue.
         iApply (GPS_PP_CAS (p:=()) (Head P) True%I Q1 (λ _ _, True)%I
                   with "kI []"); [done|done|..].
         { iSplitL; last iSplitL; last first.
-          - rewrite monPred_absolutely_unfold /=.
+          - rewrite monPred_objectively_unfold /=.
             iIntros "{$oH} !>" (?????) "[_ #$] //".
           - iNext. by iIntros (??) "_".
           - iNext. iIntros ([]).
diff --git a/theories/examples/ro_test.v b/theories/examples/ro_test.v
index 0dd1a9a99ca6d46007d1bf91d414faee8c5088e2..522b2aba218ace7a033306ac0496c7f72579eb43 100644
--- a/theories/examples/ro_test.v
+++ b/theories/examples/ro_test.v
@@ -24,6 +24,6 @@ Proof.
   { etrans; first apply namespaces.nclose_subseteq.
     by apply namespaces.ndisj_subseteq_difference. }
   iNext; iIntros (?) "[% oL']"; subst.
-  iMod ("Hclose" with "[oL]"); first by iApply absolute_absolutely.
+  iMod ("Hclose" with "[oL]"); first by iApply objective_objectively.
   iApply "Hpost"; auto.
 Admitted.
\ No newline at end of file
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index a0b674a58ee38efcc199770efcce9bccdfa6b689..94917a58437f9704e87b0845d97e170b2cc1a65d 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -654,8 +654,8 @@ Section TicketLock.
           iLeft. iIntros (z). iIntros "(NSP & _)".
           rewrite !(unf_int (NSP P γ)).
           by iDestruct "NSP" as "($ & $)".
-        - (* TODO : make iAlways able to introduce monPred_absolutely here. *)
-          rewrite monPred_absolutely_unfold. iIntros (?????) "!> (? & #$) //". }
+        - (* TODO : make iAlways able to introduce monPred_objectively here. *)
+          rewrite monPred_objectively_unfold. iIntros (?????) "!> (? & #$) //". }
 
       iNext. iIntros (n z) "(% & #NSR & Q2)".
       iDestruct "Q2" as "(% & #ES)".
@@ -726,7 +726,7 @@ Section TicketLock.
       wp_lam. wp_bind ([_]_at)%E. wp_op.
 
       iApply (GPS_SW_Read_ex (NSP P γ) with "[$kI $NSW]"); [done|done|..].
-      { rewrite monPred_absolutely_unfold. iIntros "!>" (????) "#$ //". }
+      { rewrite monPred_objectively_unfold. iIntros "!>" (????) "#$ //". }
 
       iNext. iIntros (z) "(NSW & NSP)".
       rewrite (unf_int (NSP P γ)).
diff --git a/theories/examples/tstack.v b/theories/examples/tstack.v
index 987760270239d0e3934ba80274e7ba3b25be6597..ebe362d7397665c9b79838c0dfcd34998d60256f 100644
--- a/theories/examples/tstack.v
+++ b/theories/examples/tstack.v
@@ -206,7 +206,7 @@ Section TreiberStack.
         [done|done|..].
       { iSplitL.
         - iIntros (?) "_". iLeft. by iIntros "!>" (?) "_".
-        - rewrite monPred_absolutely_unfold. setoid_rewrite <-Head_dup.
+        - rewrite monPred_objectively_unfold. setoid_rewrite <-Head_dup.
           by iIntros "!>" (?????) "[_ $]". }
 
       iNext. iIntros ([] h) "(_ & Head & _)".
@@ -232,7 +232,7 @@ Section TreiberStack.
           + iExists _, _. iFrame "ol". iNext.
             by rewrite /Reachable' (fixpoint_unfold (Reachable' P) _ _).
         - iNext. by iIntros (??) "(_ & _ & _ & ?)".
-        - rewrite monPred_absolutely_unfold. setoid_rewrite <-Head_dup.
+        - rewrite monPred_objectively_unfold. setoid_rewrite <-Head_dup.
           iIntros (?????) "!> [_ $] //".
         - by iFrame. }
 
@@ -264,7 +264,7 @@ Section TreiberStack.
           + by iDestruct "Head" as "%".
           + iDestruct "Head" as "[$ Head]".
             iDestruct "Head" as (q) "[Head _]". by iExists _, _.
-        - rewrite monPred_absolutely_unfold. setoid_rewrite <- Head_dup.
+        - rewrite monPred_objectively_unfold. setoid_rewrite <- Head_dup.
           iIntros "!>" (?????) "[_ $] //". }
 
       iNext. iIntros ([] h) "(_ & Head & Q)".
@@ -312,7 +312,7 @@ Section TreiberStack.
                 iExists A'.
                 by rewrite /Reachable (fixpoint_unfold (Reachable' P) _ _).
           - iNext. by iIntros.
-          - rewrite monPred_absolutely_unfold. setoid_rewrite <- Head_dup.
+          - rewrite monPred_objectively_unfold. setoid_rewrite <- Head_dup.
             iIntros "!>" (?????) "[_ $] //". }
 
         iNext. iIntros ([] [] _) "(_ & Head & IF)".
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index 91c616ef11e79d1a8bdd8f7255b7003f58a40bfd..aaee3cc60502ef8e4dae692746f0741fd684f762 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -126,7 +126,7 @@ Section Fractional.
       {{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌝ →
                   (∀ v, F_past l s' v ∗ P ∗ vGPS_FP l s' q ={E}=∗ Q s' v)
                   ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
                           ={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
            ∗ P ∗ vGPS_FP l s q  }}}
       ([ #(LitLoc l) ]_at) @ E
@@ -178,7 +178,7 @@ Section Fractional.
     ⎡PSCtx⎤ ⊢ {{{ (▷ ∀ s', ⌜s ⊑ s'⌝ →
                   (∀ v, F_past l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
                   ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
                           ={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
            ∗ P ∗ vGPS_FP l s q  }}}
       ([ #(LitLoc l) ]_at) @ E
@@ -199,7 +199,7 @@ Section Fractional.
       {{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌝ →
                   (∀ v, F_past l s' v ∗ P ∗ ⎡vGPS_FP l s q V⎤ ={E}=∗ Q s' v)
                   ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
                           ={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
            ∗ P ∗ ⎡vGPS_FP l s q V⎤ ∗ monPred_in V }}}
       ([ #(LitLoc l) ]_at) @ E
@@ -244,7 +244,7 @@ Section Fractional.
     ⎡PSCtx⎤ ⊢ {{{ (▷ ∀ s', ⌜s ⊑ s'⌝ →
                   (∀ v, F_past l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
                   ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
                           ={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
            ∗ P ∗ ⎡vGPS_FP l s q V⎤ ∗ monPred_in V }}}
       ([ #(LitLoc l) ]_at) @ E
@@ -369,7 +369,7 @@ Section Fractional.
                     ∗ (vGPS_FP l s'' q ={E}=∗ Q s''))
            ∗ ▷ (∀ s' v, ⌜s ⊑ s'⌝ ∗ ⌜v ≠ v_o⌝ ∗ ▷ F_past l s' v ∗ P ∗ vGPS_FP l s' q
                         ={E}=∗ R s' v)
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v ={E ∖ ↑fracN .@ l}=∗
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v ={E ∖ ↑fracN .@ l}=∗
                                                                        F_past l s' v ∗ F_past l s' v )
            ∗ P ∗ vGPS_FP l s q }}}
       (CAS #(LitLoc l) #(LitInt v_o) #(LitInt v_n)) @ E
@@ -446,7 +446,7 @@ Section Fractional.
                                                 ∗ Q s'' ∗ ▷ (F l s'' v_n) ∗ ▷ F_past l s'' v_n)
            ∗ ▷ (∀ s' v, ⌜s ⊑ s'⌝ ∗ ⌜v ≠ v_o⌝ ∗ ▷ F_past l s' v ∗ P
                         ={E ∖ ↑fracN .@ l}=∗ R s' v)
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v ={E ∖ ↑fracN .@ l}=∗
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v ={E ∖ ↑fracN .@ l}=∗
                                                                        F_past l s' v ∗ F_past l s' v )
            ∗ P ∗ vGPS_FP l s q }}}
       (CAS #(LitLoc l) #(LitInt v_o) #(LitInt v_n)) @ E
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index 0bc606bb7d0661bf0205d9bb0509b73f700bb0ac..6f5a405cb6675731068e8da0f8402891ccf06606 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -137,7 +137,7 @@ Section Plain.
               (∀ v, F_past l s' v ∗ vGPS_PP l p s' ∗ P ={E}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P
                             ={E ∖ ↑persist_locN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
                     ={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
       ∗ P ∗ vGPS_PP l p s }}}
     [ #l ]_at @ E
@@ -188,7 +188,7 @@ Section Plain.
               (∀ v, F_past l s' v ∗ P ={E ∖ ↑persist_locN .@ l}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P
                             ={E ∖ ↑persist_locN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
                     ={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
       ∗ P ∗ vGPS_PP l p s }}}
     [ #l ]_at @ E
@@ -258,7 +258,7 @@ Section Plain.
                   (vGPS_PP l p s'' ={E}=∗ Q s''))
       ∗ ▷(∀ s' v, ⌜s ⊑ s'⌝ ∗ ⌜v ≠ v_o⌝ ∗ ▷ F_past l s' v ∗ vGPS_PP l p s' ∗ P
                       ={E}=∗ R s' v)
-      ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+      ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
                   ={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
       ∗ P ∗ vGPS_PP l p s }}}
     (CAS #l #v_o #v_n) @ E
@@ -339,7 +339,7 @@ Section Plain.
                         ∗ Q s'' ∗ ▷ (F l s'' v_n) ∗ ▷ F_past l s'' v_n)
       ∗ ▷(∀ s' v, ⌜s ⊑ s'⌝ ∗ ⌜v ≠ v_o⌝ ∗ ▷ F_past l s' v ∗ P
                       ={E ∖ ↑persist_locN .@ l}=∗ R s' v)
-      ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+      ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
                   ={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
       ∗ P ∗ vGPS_PP l p s }}}
     (CAS #l #v_o #v_n) @ E
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 517f21e7102f0793fb8df897b1da4161f860f34a..27937e56d1b75e92b1447214549444f2098b39f6 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -116,7 +116,7 @@ Section Gname_StrongSW.
 
   Lemma GPS_nFWP_ExRead γ l s q (E : coPset)
       (HN : ↑physN ⊆ E) (HNl: ↑fracN .@ l ⊆ E):
-  {{{ ⎡PSCtx⎤ ∗ ▷ ∀ᵢ (∀ v, F_past γ l s v ={E ∖ ↑fracN .@ l}=∗
+  {{{ ⎡PSCtx⎤ ∗ ▷ <obj> (∀ v, F_past γ l s v ={E ∖ ↑fracN .@ l}=∗
                    F_past γ l s v ∗ F_past γ l s v ) ∗ vGPS_nFWP γ l s q }}}
     ([ #l ]_at) @ E
   {{{ v, RET #v ;
@@ -382,7 +382,7 @@ Section Gname_StrongSW.
   {{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌝ →
               (∀ v, F_past γ l s' v ∗ P ∗ vGPS_nFRP γ l s' q ={E}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-         ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
+         ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
             ={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
       ∗ P ∗ vGPS_nFRP γ l s q  }}}
     ([ #l ]_at) @ E
@@ -424,7 +424,7 @@ Section Gname_StrongSW.
   {{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌝ →
               (∀ v, F_past γ l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-         ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
+         ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
             ={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
       ∗ P ∗ vGPS_nFRP γ l s q  }}}
     ([ #l ]_at) @ E
@@ -446,7 +446,7 @@ Section Gname_StrongSW.
   {{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌝ →
               (∀ v, F_past γ l s' v ∗ P ∗ ⎡vGPS_nFRP γ l s1 q V⎤ ={E}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-         ∗ ▷ ∀ᵢ (∀ s' v, ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌝ ∗ F_past γ l s' v
+         ∗ ▷ <obj> (∀ s' v, ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌝ ∗ F_past γ l s' v
             ={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
       ∗ P ∗ monPred_in V ∗ ⎡vGPS_nFRP γ l s1 q V⎤ ∗ PrtSeen γ s2  }}}
     ([ #l ]_at) @ E
@@ -519,7 +519,7 @@ Section Gname_StrongSW.
   ⎡PSCtx⎤ ⊢ {{{ (▷ ∀ s', ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌝ →
               (∀ v, F_past γ l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-         ∗ ▷ ∀ᵢ (∀ s' v, ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌝ ∗ F_past γ l s' v
+         ∗ ▷ <obj> (∀ s' v, ⌜s1 ⊑ s' ∧ s2 ⊑ s'⌝ ∗ F_past γ l s' v
             ={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
       ∗ P ∗ monPred_in V ∗ ⎡vGPS_nFRP γ l s1 q V⎤ ∗ PrtSeen γ s2  }}}
     ([ #l ]_at) @ E
@@ -539,7 +539,7 @@ Section Gname_StrongSW.
   {{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌝ →
               (∀ v, F_past γ l s' v ∗ P ∗ ⎡vGPS_nFRP γ l s q V⎤ ={E}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-         ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
+         ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
             ={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
       ∗ P ∗ monPred_in V ∗ ⎡vGPS_nFRP γ l s q V⎤  }}}
     ([ #l ]_at) @ E
@@ -585,7 +585,7 @@ Section Gname_StrongSW.
   ⎡PSCtx⎤ ⊢ {{{ (▷ ∀ s', ⌜s ⊑ s'⌝ →
               (∀ v, F_past γ l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F γ l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-         ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
+         ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
             ={E ∖ ↑fracN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
       ∗ P ∗ monPred_in V ∗ ⎡vGPS_nFRP γ l s q V⎤ }}}
     ([ #l ]_at) @ E
@@ -761,7 +761,7 @@ Section Gname_StrongSW_Param.
 
   Lemma GPS_nSW_ExRead l γ p s (E : coPset)
       (HN : ↑physN ⊆ E) (HNl: ↑persist_locN .@ l ⊆ E):
-  {{{ ⎡PSCtx⎤ ∗ ▷ ∀ᵢ (∀ v, F_past γ l s v ={E ∖ ↑persist_locN .@ l}=∗
+  {{{ ⎡PSCtx⎤ ∗ ▷ <obj> (∀ v, F_past γ l s v ={E ∖ ↑persist_locN .@ l}=∗
                    F_past γ l s v ∗ F_past γ l s v ) ∗ vGPS_nWSP γ l p s }}}
     ([ #l ]_at) @ E (* TODO: can be non-atomic *)
   {{{ v, RET #v ;
@@ -799,7 +799,7 @@ Section Gname_StrongSW_Param.
               (∀ v, F_past γ l s' v ∗ P ∗ vGPS_nRSP γ l p s' ={E}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F γ l s'' v ∗ P
                                        ={E ∖ ↑persist_locN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
               ={E ∖ ↑persist_locN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
            ∗ P ∗ vGPS_nRSP γ l p s }}}
     ([ #l ]_at) @ E
@@ -842,7 +842,7 @@ Section Gname_StrongSW_Param.
               (∀ v, F_past γ l s' v ∗ P ={E ∖ ↑ persist_locN .@ l}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F γ l s'' v ∗ P
                                        ={E ∖ ↑persist_locN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past γ l s' v
               ={E ∖ ↑persist_locN .@ l}=∗ F_past γ l s' v ∗ F_past γ l s' v )
            ∗ P ∗ vGPS_nRSP γ l p s }}}
     ([ #l ]_at) @ E
@@ -1090,7 +1090,7 @@ Section SingleWriter.
 
   Lemma GPS_SW_Read_ex l s (E : coPset)
       (HN : ↑physN ⊆ E) (HNl: ↑persist_locN .@ l ⊆ E):
-  {{{ ⎡PSCtx⎤ ∗ ▷ ∀ᵢ (∀ v, F_past l s v ={E ∖ ↑persist_locN .@ l}=∗
+  {{{ ⎡PSCtx⎤ ∗ ▷ <obj> (∀ v, F_past l s v ={E ∖ ↑persist_locN .@ l}=∗
                    F_past l s v ∗ F_past l s v ) ∗ vGPS_WSP l s }}}
     ([ #l ]_at) @ E
   {{{ v, RET #v ;
@@ -1161,7 +1161,7 @@ Section SingleWriter.
               (∀ v, F_past l s' v ∗ P ∗ vGPS_RSP l s' ={E}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P
                                        ={E ∖ ↑persist_locN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
               ={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
            ∗ P ∗ vGPS_RSP l s }}}
     ([ #l ]_at) @ E
@@ -1206,7 +1206,7 @@ Section SingleWriter.
               (∀ v, F_past l s' v ∗ P ={E ∖ ↑ persist_locN .@ l}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P
                                        ={E ∖ ↑persist_locN .@ l}=∗ False))
-           ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+           ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
               ={E ∖ ↑persist_locN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
            ∗ P ∗ vGPS_RSP l s }}}
     ([ #l ]_at) @ E
@@ -1342,7 +1342,7 @@ Section SingleWriter.
   {{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌝ →
               (∀ v, F_past l s' v ∗ P ∗ vGPS_FRP l s' q ={E}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-         ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+         ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
             ={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
       ∗ P ∗ vGPS_FRP l s q  }}}
     ([ #l ]_at) @ E
@@ -1387,7 +1387,7 @@ Section SingleWriter.
   {{{ ⎡PSCtx⎤ ∗ (▷ ∀ s', ⌜s ⊑ s'⌝ →
               (∀ v, F_past l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
             ∨ (∀ s'' v, ⌜s' ⊑ s''⌝ → F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
-         ∗ ▷ ∀ᵢ (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
+         ∗ ▷ <obj> (∀ s' v, ⌜s ⊑ s'⌝ ∗ F_past l s' v
             ={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
       ∗ P ∗ vGPS_FRP l s q  }}}
     ([ #l ]_at) @ E
@@ -1405,7 +1405,7 @@ Section SingleWriter.
 
   Lemma GPS_FWP_ExRead l s q (E : coPset)
       (HN : ↑physN ⊆ E) (HNl: ↑fracN .@ l ⊆ E):
-  {{{ ⎡PSCtx⎤ ∗ ▷ ∀ᵢ (∀ v, F_past l s v ={E ∖ ↑fracN .@ l}=∗
+  {{{ ⎡PSCtx⎤ ∗ ▷ <obj> (∀ v, F_past l s v ={E ∖ ↑fracN .@ l}=∗
                    F_past l s v ∗ F_past l s v ) ∗ vGPS_FWP l s q }}}
     ([ #l ]_at) @ E
   {{{ v, RET #v ;
diff --git a/theories/invariants.v b/theories/invariants.v
index fb5cc9b168c15aaf3db50982f7667e4f7826f475..4c807e082a8ba9cf01138bd65df5b13c1da08e8a 100644
--- a/theories/invariants.v
+++ b/theories/invariants.v
@@ -7,30 +7,30 @@ Section Invariants.
   Context {Σ : gFunctors} `{fG : !foundationG Σ} `{W : invG.invG Σ}.
   Definition inv N (P : vProp Σ) : vProp Σ := ⎡invariants.inv N (∀ V, monPred_at P V)⎤%I.
 
-  Lemma inv_alloc N (E : coPset) (P : vProp Σ) : ▷ (∀ᵢ P) -∗ |={E}=> inv N P.
+  Lemma inv_alloc N (E : coPset) (P : vProp Σ) : ▷ (<obj> P) -∗ |={E}=> inv N P.
   Proof.
-    iIntros "H". rewrite monPred_absolutely_unfold /= -embed_later.
+    iIntros "H". rewrite monPred_objectively_unfold /= -embed_later.
     by iMod (invariants.inv_alloc with "H") as "$".
   Qed.
 
   Lemma inv_alloc_open N (E : coPset) (P : vProp Σ) :
-    ↑N ⊆ E → (|={E,E ∖ ↑N}=> inv N P ∗ (▷ (∀ᵢ P) ={E ∖ ↑N,E}=∗ True))%I.
+    ↑N ⊆ E → (|={E,E ∖ ↑N}=> inv N P ∗ (▷ (<obj> P) ={E ∖ ↑N,E}=∗ True))%I.
   Proof.
-    rewrite monPred_absolutely_unfold /= -embed_later.
+    rewrite monPred_objectively_unfold /= -embed_later.
     iIntros (?). iMod (invariants.inv_alloc_open) as "[$ Close]"; [done|].
     iIntros "!> H". by iMod ("Close" with "H").
   Qed.
 
  Lemma inv_open (E : coPset) N (P : vProp Σ) :
-   ↑N ⊆ E → inv N P -∗ |={E,E ∖ ↑N}=> ▷ (∀ᵢ P) ∗ (▷ (∀ᵢ P) ={E ∖ ↑N,E}=∗ True).
+   ↑N ⊆ E → inv N P -∗ |={E,E ∖ ↑N}=> ▷ (<obj> P) ∗ (▷ (<obj> P) ={E ∖ ↑N,E}=∗ True).
  Proof.
-   iIntros (?) "H". rewrite monPred_absolutely_unfold /= -embed_later.
+   iIntros (?) "H". rewrite monPred_objectively_unfold /= -embed_later.
    iMod (invariants.inv_open with "H") as "[$ Close]"; [done|].
    iIntros "!> H". by iMod ("Close" with "H").
  Qed.
 
  (* TODO : this should be removed and replaced with the general iAlways
     tactic. *)
- Lemma absolutely_entails (P Q : vProp Σ) : (P -∗ Q) -> bi_valid (∀ᵢ (P -∗ Q))%I.
+ Lemma objectively_entails (P Q : vProp Σ) : (P -∗ Q) -> bi_valid (<obj> (P -∗ Q))%I.
  Proof. iStartProof (iProp _). iIntros (H V ???). rewrite H. auto. Qed.
 End Invariants.
diff --git a/theories/logically_atomic.v b/theories/logically_atomic.v
index 7961c732c5dd943e753dc4ed66ef10d768ae3993..6f2896243312ca7a437f3afd56e6a300e3219414 100644
--- a/theories/logically_atomic.v
+++ b/theories/logically_atomic.v
@@ -70,7 +70,7 @@ Proof.
     iApply "Hclose"; iFrame.
 Qed.
 
-Lemma LA_Inv {A} (α : A -> vProp Σ) β Ei Eo e N R {_ : Absolute R}:
+Lemma LA_Inv {A} (α : A -> vProp Σ) β Ei Eo e N R {_ : Objective R}:
   ↑N ## Ei ->
   atomic_wp (fun x => ▷R ∗ α x)%I (fun x v => ▷R ∗ β x v)%I Ei Eo e -∗
   atomic_wp (fun x => inv N R ∗ α x)%I β (↑N ∪ Ei) Eo e.
@@ -83,7 +83,7 @@ Proof.
   iPoseProof (inv_open (↑N ∪ Ei) with "Hinv") as "HR".
   { apply union_subseteq_l. }
   iMod "HR" as "[HR HcloseR]".
-  iDestruct (monPred_absolutely_elim with "HR") as "HR".
+  iDestruct (monPred_objectively_elim with "HR") as "HR".
   assert (Ei = (↑N ∪ Ei) ∖ ↑N) as <-.
   { rewrite difference_union_distr_l_L difference_diag_L union_empty_l_L
             difference_disjoint_L; done. }
@@ -91,11 +91,11 @@ Proof.
   iExists x; iFrame; iSplit.
   - iIntros "[HR Hx]".
     iMod ("HcloseR" with "[HR]").
-    { by iApply absolute_absolutely. }
+    { by iApply objective_objectively. }
     iApply "Hclose"; auto.
   - iIntros (v) "[HR Hv]".
     iMod ("HcloseR" with "[HR]").
-    { by iApply absolute_absolutely. }
+    { by iApply objective_objectively. }
     iApply "Hclose"; auto.
 Qed.
 
@@ -132,7 +132,7 @@ Proof.
 Qed.
 
 Lemma LA_Inv' {A} β Ei Eo e N (R : A -> vProp Σ) Ei'
-  {_ : ∀ x, Absolute (R x)} {_ : ∀ x, Timeless (R x)}:
+  {_ : ∀ x, Objective (R x)} {_ : ∀ x, Timeless (R x)}:
   ↑N ## Ei -> ↑N ∪ Ei ⊆ Ei' ->
   atomic_wp (fun x => R x)%I (fun x v => (∃y, R y) ∗ β x v)%I Ei Eo e -∗
   atomic_wp (fun _ : unit => inv N (∃x, R x))%I (fun _ v => ∃x, β x v) Ei' Eo e.
@@ -147,18 +147,18 @@ Proof.
   iPoseProof (inv_open (↑N ∪ Ei) with "Hinv") as "HR".
   { apply union_subseteq_l. }
   iMod "HR" as "[>HR HcloseR]".
-  iDestruct (monPred_absolutely_elim with "HR") as (a) "HR".
+  iDestruct (monPred_objectively_elim with "HR") as (a) "HR".
   assert (Ei = (↑N ∪ Ei) ∖ ↑N) as <-.
   { by rewrite difference_union_distr_l_L difference_diag_L union_empty_l_L
                difference_disjoint_L. }
   iModIntro. iExists a; iFrame; iSplit.
   - iIntros "HR".
     iMod ("HcloseR" with "[HR]").
-    { iApply absolute_absolutely; by iExists a. }
+    { iApply objective_objectively; by iExists a. }
     iApply "Hclose"; auto.
   - iIntros (v) "[HR Hv]".
     iMod ("HcloseR" with "[HR]").
-    { by iApply absolute_absolutely. }
+    { by iApply objective_objectively. }
     iApply "Hclose"; auto.
 Qed.
 End LA_rules.