diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 78407980bc72db35aaf0e9ac9fae50d0f2244844..3bf479c55bc21cc7bdf38a9eef4acdd393521fb7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -27,25 +27,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.11.0:
+build-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.11.0"
-    OPAM_PKG: "coq-gpfsl"
+    OPAM_PINS: "coq version 8.11.0   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#ci/robbert/merge_sbi_new"
   tags:
   - fp-timing
 
-build-coq.8.10.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.10.2"
-
-build-iris.dev:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.11.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV   coq-orc11.dev git git+https://gitlab.mpi-sws.org/iris/orc11.git#$ORC11_REV"
-  except:
-  only:
-  - triggers
-  - schedules
-  - api
diff --git a/theories/base_logic/vprop.v b/theories/base_logic/vprop.v
index a66f58851469c3f9d7a1f0b7c84a7fbbf6cf1742..f2a014a36743829e04a8e2fcde3beb7367bea34b 100644
--- a/theories/base_logic/vprop.v
+++ b/theories/base_logic/vprop.v
@@ -17,7 +17,6 @@ Canonical Structure view_bi_index :=
 Definition vProp Σ := monPred view_bi_index (uPredI (iResUR Σ)).
 Definition vPropO Σ := monPredO view_bi_index (uPredI (iResUR Σ)).
 Definition vPropI Σ := monPredI view_bi_index (uPredI (iResUR Σ)).
-Definition vPropSI Σ := monPredSI view_bi_index (uPredSI (iResUR Σ)).
 
 Hint Extern 10 (IsBiIndexRel _ _) => unfold IsBiIndexRel; solve_lat
             : typeclass_instances.
@@ -25,7 +24,7 @@ Hint Extern 10 (IsBiIndexRel _ _) => unfold IsBiIndexRel; solve_lat
 (* SOME big_op lemmas *)
 From iris.bi Require Import big_op.
 
-Lemma big_sepM_dup {PROP: sbi} `{Countable K} {A: Type} (φ: K → A → PROP) (m: gmap K A) k a q
+Lemma big_sepM_dup {PROP: bi} `{Countable K} {A: Type} (φ: K → A → PROP) (m: gmap K A) k a q
   (In: m !! k = Some a)
   : ▷?q (φ k a -∗ φ k a ∗ φ k a) ∗ ▷?q ([∗ map] k' ↦ v' ∈ m, φ k' v')
     ⊢ ▷?q φ k a ∗ ▷?q ([∗ map] k' ↦ v' ∈ m, φ k' v').
diff --git a/theories/base_logic/weakestpre.v b/theories/base_logic/weakestpre.v
index 6fced49644ce7cab6c351791d734b748778c3f54..27755f3800418644011992d8580d115200f75fd9 100644
--- a/theories/base_logic/weakestpre.v
+++ b/theories/base_logic/weakestpre.v
@@ -129,7 +129,7 @@ Proof.
   by iApply ("IH" with "Hs' WP").
 Qed.
 
-Program Definition wp_def tid E e Φ : vPropSI Σ :=
+Program Definition wp_def tid E e Φ : vPropI Σ :=
   MonPred (λ V,
     ∀ 𝓥, ⌜V ⊑ 𝓥.(cur)⌝ -∗ own tid (● to_latT 𝓥) -∗ seen 𝓥 -∗
       WP e at 𝓥 @ E {{ λ v𝓥', let '(v at 𝓥') := v𝓥' return _ in
diff --git a/theories/examples/na_stack.v b/theories/examples/na_stack.v
index a06d57ca4fc89d0406b6962a629a4951dc4dc664..e440607b5a2028ad3b37cd9fa933f0aad828fb18 100644
--- a/theories/examples/na_stack.v
+++ b/theories/examples/na_stack.v
@@ -58,7 +58,7 @@ Proof.
   destruct A as [|v A]; [done|].
   apply bi.exist_ne => ?.
   repeat (apply bi.sep_ne; [done|]).
-  apply bi.later_contractive. destruct n => //. by apply H.
+  f_contractive. by apply H.
 Qed.
 
 Definition NAStack_def := fixpoint NAStack'.
diff --git a/theories/examples/treiber_stack.v b/theories/examples/treiber_stack.v
index e15533479823f8607c9c9fe4454c926ee516057a..1ca3cf28ea45c1b22b3d9f1c2d2b20c713cb780f 100644
--- a/theories/examples/treiber_stack.v
+++ b/theories/examples/treiber_stack.v
@@ -68,7 +68,7 @@ Proof.
   repeat (apply bi.sep_ne; [done|]).
   do 2 (apply bi.exist_ne => ?).
   repeat (apply bi.sep_ne; [done|]).
-  apply bi.later_contractive. destruct n => //. by apply H.
+  f_contractive. by apply H.
 Qed.
 
 Definition Reachable := fixpoint Reachable'.
@@ -91,7 +91,7 @@ Proof.
   apply bi.sep_ne; [done|].
   apply bi.exist_ne => ?.
   apply bi.sep_ne; [done|].
-  apply bi.later_contractive. destruct n => //. by apply H.
+  f_contractive. by apply H.
 Qed.
 
 Definition ReachableD := fixpoint ReachableD'.
diff --git a/theories/gps/model_defs.v b/theories/gps/model_defs.v
index 831bb92dc3be752d7b5c7dfb8409c3c57e66091d..0d9aaf8ff0c5e594e865e7d30e60bbbae971ee5f 100644
--- a/theories/gps/model_defs.v
+++ b/theories/gps/model_defs.v
@@ -639,8 +639,7 @@ Program Example intExample Σ : interpO Σ unitProtocol :=
     (λ (F : interpO Σ unitProtocol) b l γ t s v, ∃ c, ⌜c = #1⌝ ∗ ▷ F b l γ t s v)%I _.
 Next Obligation.
   repeat intro.
-  apply bi.exist_ne => ? . apply bi.sep_ne; [done|]. apply bi.later_contractive.
-  destruct n; [done|]. apply H.
+  apply bi.exist_ne => ? . apply bi.sep_ne; [done|]. f_contractive. apply H.
 Qed.
 
 Lemma alloc_local_singleton_seen_local l t m V: