diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 1184346842f079d07698a43b48fb3a98d430ef01..f6862143fd02831ecfaf565b7a0162615926e824 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,8 +10,8 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2022-08-03.0.949ab7bc") | (= "dev") }
-  "coq-orc11" { (= "dev.2022-07-30.0.e76351a5") | (= "dev") }
+  "coq-iris"  { (= "dev.2022-08-10.1.b06a6961") | (= "dev") }
+  "coq-orc11" { (= "dev.2022-08-05.0.c8ba00f9") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/logic/logatom.v b/theories/logic/logatom.v
index b9a5ad9040bfc528468bdcb04be0233b34a1d9ef..0ded535fd1b1ba6f49e75002a3758d8d7d8134b8 100644
--- a/theories/logic/logatom.v
+++ b/theories/logic/logatom.v
@@ -125,13 +125,13 @@ Section lemmas.
     iApply atomic_update_mask_weaken; last done. set_solver.
   Qed.
 
-  (* Atomic triples imply sequential triples if the precondition is laterable. *)
-  Lemma atomic_wp_seq e tid E α β POST f {HL : ∀.. x, Laterable (α x)}
+  (* Atomic triples imply sequential triples. *)
+  Lemma atomic_wp_seq e tid E α β POST f
     (Sub: ↑histN ⊆ ⊤ ∖ E) :
     atomic_wp e tid E α β POST f -∗
     ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ POST x y -∗ Φ (f x y)) -∗ WP e @ tid; ⊤ {{ Φ }}.
   Proof.
-    rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
+    iIntros "Hwp" (Φ x) "Hα HΦ".
     iApply wp_frame_wand_l. iSplitL "HΦ"; first iAccu. iApply "Hwp".
     iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
     rewrite !tele_app_bind. iIntros "HP HΦ". by iApply ("HΦ" with "Hβ HP").
@@ -139,7 +139,7 @@ Section lemmas.
 
   (** This version matches the Texan triple, i.e., with a later in front of the
   [(∀.. y, β x y -∗ Φ (f x y))]. *)
-  Lemma atomic_wp_seq_step e tid E α β POST f {HL : ∀.. x, Laterable (α x)}
+  Lemma atomic_wp_seq_step e tid E α β POST f
     (Sub: ↑histN ⊆ ⊤ ∖ E) :
     TCEq (to_val e) None →
     atomic_wp e tid E α β POST f -∗
diff --git a/theories/logic/proofmode.v b/theories/logic/proofmode.v
index b48f163cb5b92a20e97dcf519ee98238fb6ab5d8..3bbd117b3ec6ec66361a096252e00032e64c315b 100644
--- a/theories/logic/proofmode.v
+++ b/theories/logic/proofmode.v
@@ -226,25 +226,11 @@ Tactic Notation "wp_smart_apply" open_constr(lem) :=
   wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; simpl)
                   ltac:(fun cont => wp_pure _; []; cont ()).
 
-(** Tactic tailored for atomic triples: the first, simple one just runs
-[iAuIntro] on the goal, as atomic triples always have an atomic update as their
-premise.  The second one additionaly does some framing: it gets rid of [Hs] from
-the context, which is intended to be the non-laterable assertions that iAuIntro
-would choke on.  You get them all back in the continuation of the atomic
-operation. *)
+(** Tactic tailored for atomic triples: just runs [iAuIntro] on the goal, as
+atomic triples always have an atomic update as their premise. *)
 Tactic Notation "awp_apply" open_constr(lem) :=
   wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
   last iAuIntro.
-(* Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
-  (* Convert "list of hypothesis" into specialization pattern. *)
-  let Hs := words Hs in
-  let Hs := eval vm_compute in (INamed <$> Hs) in
-  wp_apply_core lem
-    ltac:(fun H =>
-      iApply (wp_frame_wand with
-        [SGoal $ SpecGoal GSpatial false [] Hs false]); [iAccu|iApplyHyp H])
-    ltac:(fun cont => fail);
-  last iAuIntro. *)
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(Hm) constr(H) constr(Hf) :=
   iStartProof;