diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 2dd7897bbc9429915ce7c508a32e86fb8041be27..bcce9cd5c02d17c1b9cbb807906367a917b1f665 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.2025-03-25.0.79d33e24") | (= "dev") }
+  "coq-iris"  { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
 ]
 
 build: ["./make-package" "gpfsl" "-j%{jobs}%"]
diff --git a/gpfsl-examples/algebra/mono_list_list.v b/gpfsl-examples/algebra/mono_list_list.v
index 83a9b2fb50c1498704d7ac2edeb2f1d6a9e1db67..3a8fa9b04943d481a33e1d690a4aecf084ab54b0 100644
--- a/gpfsl-examples/algebra/mono_list_list.v
+++ b/gpfsl-examples/algebra/mono_list_list.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export auth max_prefix_list.
+From iris.algebra Require Export auth max_prefix_list stepindex_finite.
 From iris.algebra Require Import updates local_updates proofmode_classes.
 
 From iris.prelude Require Import options.
diff --git a/gpfsl-examples/lock/proof_ticket_lock_gps.v b/gpfsl-examples/lock/proof_ticket_lock_gps.v
index 44bd1a55dfcfd9531e32f82617b5db2d001b2dc5..ed195f7fc7253a7ff092404e9354d461ea0873c2 100644
--- a/gpfsl-examples/lock/proof_ticket_lock_gps.v
+++ b/gpfsl-examples/lock/proof_ticket_lock_gps.v
@@ -370,7 +370,7 @@ Proof.
   apply bi.sep_ne; [done|].
   repeat (apply bi.exist_ne => ?).
   apply GPS_iSP_Writer_contractive; [done|].
-  dist_later_fin_intro. eapply H; si_solver.
+  dist_later_fin_intro. eapply H, SIdx.lt_succ_diag_r.
 Qed.
 
 Definition NSP P γ : interpO Σ natProtocol := fixpoint (NSP' P γ).
diff --git a/gpfsl-examples/queue/proof_ms_gps.v b/gpfsl-examples/queue/proof_ms_gps.v
index f885eb5a03def42e8d200c13df027ab25b79573a..9628ad16a8618656b5106a9a1406e4e5273b754e 100644
--- a/gpfsl-examples/queue/proof_ms_gps.v
+++ b/gpfsl-examples/queue/proof_ms_gps.v
@@ -83,7 +83,7 @@ Proof.
   apply bi.sep_ne; [done|].
   do 2 (apply bi.exist_ne => ?).
   apply GPS_iPP_contractive.
-  dist_later_fin_intro. eapply H; si_solver.
+  dist_later_fin_intro. eapply H, SIdx.lt_succ_diag_r.
 Qed.
 
 Definition Link : ∀ γ, interpO Σ LinkProtocol := fixpoint Link'.
diff --git a/gpfsl/algebra/to_agree.v b/gpfsl/algebra/to_agree.v
index 24787c537f6a650c1ba5c7ced516b9ebe5881bd9..80f55dac2e4e3b980bfedd3e6073eb6303852606 100644
--- a/gpfsl/algebra/to_agree.v
+++ b/gpfsl/algebra/to_agree.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import agree gmap local_updates.
+From iris.algebra Require Import agree gmap local_updates stepindex_finite.
 
 Require Import iris.prelude.options.
 
diff --git a/gpfsl/gps/model_defs.v b/gpfsl/gps/model_defs.v
index a17804bda12d31b0d30e7b29bbd1e28d89b62b3e..88070ce9cbd77669a297be97ed9a667acf476890 100644
--- a/gpfsl/gps/model_defs.v
+++ b/gpfsl/gps/model_defs.v
@@ -454,7 +454,7 @@ Section recursive.
   Proof. constructor; repeat intro; exact True%I. Qed.
 End recursive.
 Program Example intExample Σ : interpO Σ unitProtocol :=
-  @fixpoint _ _ _
+  @fixpoint _ _ _ _
     (λ (F : interpO Σ unitProtocol) b l γ t s v, ∃ c, ⌜c = #1⌝ ∗ ▷ F b l γ t s v)%I _.
 Next Obligation.
   intros ???? H. repeat intro.
diff --git a/gpfsl/logic/na_invariants.v b/gpfsl/logic/na_invariants.v
index 090ebb98688fb5ac3a3d7864314611d4ae72cf5e..b87498d30592b62366a602fbfe1eca5e30ae66db 100644
--- a/gpfsl/logic/na_invariants.v
+++ b/gpfsl/logic/na_invariants.v
@@ -11,12 +11,12 @@ Require Import iris.prelude.options.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Vw `{!LatBottom bot} Σ :=
-  { na_inv_enable_inG : inG Σ (@discrete_funR positive (λ _, authUR (latUR Vw)));
+  { na_inv_enable_inG : inG Σ (discrete_funR (λ _ : positive, authUR (latUR Vw)));
     na_inv_disable_inG : inG Σ (excl_authR (latO Vw)) }.
 Local Existing Instances na_inv_enable_inG na_inv_disable_inG.
 
 Definition na_invΣ Vw `{!LatBottom bot} : gFunctors :=
-  #[ GFunctor (constRF (@discrete_funR positive (λ _, authUR (latUR Vw))));
+  #[ GFunctor (constRF (discrete_funR (λ _ : positive, authUR (latUR Vw))));
      GFunctor (constRF (excl_authR (latO Vw))) ].
 Global Instance subG_na_invG Vw `{!LatBottom bot} Σ :
   subG (na_invΣ Vw) Σ → na_invG Vw Σ.
@@ -109,7 +109,7 @@ Section proofs.
   Proof.
     iIntros "HP".
     iDestruct (monPred_in_intro with "HP") as (V) "[#HV HP]".
-    iMod (own_unit (@discrete_funUR positive (λ _, authUR (latUR Vw))) p) as "Hempty".
+    iMod (own_unit (discrete_funUR (λ _ : positive, authUR (latUR Vw))) p) as "Hempty".
     iMod (own_alloc (● None)) as (γ) "Hdis"; [by apply auth_auth_valid|].
     destruct (fresh_inv_name ∅ N) as (i & _ & HiN). unfold na_inv.
     iExists i, V, γ. iFrame "# %". iMod (inv_alloc N with "[-]") as "$"; [|done].
@@ -156,7 +156,7 @@ Section proofs.
     iDestruct "Htoki" as (Vi) "[Hown Hdis1]".
     iCombine "Hdis1 Hdis2" gives %EQVi%excl_auth_agree%(inj to_latT).
     (* FIXME : rewrite EQVi should work. *)
-    assert (@discrete_fun_singleton _ _ (λ _, _) i (● to_latT Vi) ≡
+    assert (@discrete_fun_singleton _ _ _ (λ _, _) i (● to_latT Vi) ≡
             discrete_fun_singleton i (● to_latT (Vs i))) as -> by by f_equiv; rewrite EQVi.
     iMod (own_update_2 with "Hdis1 Hdis2") as "Hdis".
     { apply auth_update_dealloc, delete_option_local_update, _. }