diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 17ad0c708e38ed6a690800836ad3973868fa4078..61db5e555f4186ecf7bda74c0c383e9b168a5dd2 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2023-10-13.0.d199a249") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-10-16.0.4a17223a") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/coq-orc11.opam b/coq-orc11.opam
index d3e37d10a494aea62ad9e41505882b5839b141cb..e507db0e8c7ee29ed1312c4a526f40af9f0e50b4 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
 
 depends: [
-  "coq-stdpp" { (= "dev.2023-10-13.1.03757caf") | (= "dev") }
+  "coq-stdpp" { (= "dev.2023-10-14.6.32edabf7") | (= "dev") }
 ]
 
 build: ["./make-package" "orc11" "-j%{jobs}%"]
diff --git a/gpfsl-examples/sflib.v b/gpfsl-examples/sflib.v
index 8dc7a20985602fa6a30eea2bcf498e8d0dc41f8e..4c9559a46c62a14c56f96ff4fc8590ed88cc77e0 100644
--- a/gpfsl-examples/sflib.v
+++ b/gpfsl-examples/sflib.v
@@ -117,38 +117,6 @@ Ltac clarify :=
     | H1: ?x = Some _, H2: ?x = Some _ |- _ => rewrite H2 in H1; sflib__clarify1
   end.
 
-(** Kill simple goals that require up to two econstructor calls. *)
-
-(* from CompCert-2.4/lib/Coqlib.v *)
-Ltac inv H := inversion H; clear H; subst.
-
-Ltac hinv x := move x at bottom; inversion x; clarify.
-
-Tactic Notation "hinv" ident(a) :=
-  (hinv a).
-Tactic Notation "hinv" ident(a) ident(b) :=
-  (hinv a; hinv b).
-Tactic Notation "hinv" ident(a) ident(b) ident(c) :=
-  (hinv a; hinv b c).
-Tactic Notation "hinv" ident(a) ident(b) ident(c) ident(d) :=
-  (hinv a b; hinv c d).
-
-Ltac hinvc x := hinv x; clear x.
-
-Tactic Notation "hinvc" ident(a) :=
-  (hinvc a).
-Tactic Notation "hinvc" ident(a) ident(b) :=
-  (hinvc a; hinvc b).
-Tactic Notation "hinvc" ident(a) ident(b) ident(c) :=
-  (hinvc a; hinvc b c).
-Tactic Notation "hinvc" ident(a) ident(b) ident(c) ident(d) :=
-  (hinvc a b; hinvc c d).
-Tactic Notation "hinvc" ident(a) ident(b) ident(c) ident(d) ident(e) :=
-  (hinvc a b c; hinvc d e).
-
-Ltac simpls  := simpl in *; try done.
-Ltac ins := simpl in *; try done; intros.
-
 Tactic Notation "case_eq" constr(x) := case_eq (x).
 
 Tactic Notation "case_eq" constr(x) "as" simple_intropattern(H) :=
@@ -418,7 +386,6 @@ Ltac des_ifs :=
     end.
 
 Ltac desf := clarify; des; des_ifs.
-Ltac isd := ins; desf.
 
 (** Create a copy of hypothesis [H]. *)
 Tactic Notation "dup" hyp(H) :=
@@ -731,7 +698,6 @@ Tactic Notation "s" := simpl.
 Tactic Notation "s" ident(a) := simpl a.
 Tactic Notation "s" constr(t) := simpl t.
 Tactic Notation "s" "in" hyp(H) := simpl in H.
-Tactic Notation "ss" := simpls.
 Tactic Notation "r" := red.
 Tactic Notation "r" "in" hyp(H) := red in H.
 Tactic Notation "rr" := repeat red.
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index d615e49042fc4e3ecdd518b1ec29792fe57f86d5..3fe11fb6f8c9469482e95fb78ba8f5c58b045804 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -2533,7 +2533,7 @@ Proof.
                 { by apply nil_snoc in Hnil. }
                 apply app_inj_tail in ORD as [<- <-].
                 apply lookup_last_Some_2 in EVENT as ->.
-                inv RUN; [|done].
+                inv RUN.
                 specialize (stack_interp_functional _ _ _ _ _ INTERP' XO_INTERP) as [= ? <-].
                 by apply EMPTYING_WRITE.
              ++ intros. assert (stk2' = []) as ->. { auto. }