diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2cf821db8e41aac691b35b7cb35a7e3b3a4af5f3..840569328a77ffa3cada4c457f70ce858a698559 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -27,7 +27,7 @@ variables:
 
 ## Build jobs
 
-build-coq.8.10.2:
+build-coq.8.11.2:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.10.2"
+    OPAM_PINS: "coq version 8.11.2"
diff --git a/opam b/opam
index 8bcc12aef3948a24d81baf3be4eaf846b14d8bce..215f078997e15c4279fb79180244d84f7055610c 100644
--- a/opam
+++ b/opam
@@ -10,7 +10,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
 synopsis: "This is the Coq development of the Iris Project"
 
 depends: [
-  "coq" { (= "8.10.2") }
+  "coq" { (= "8.11.2") }
   "coq-stdpp" { (= "1.3.0") }
 ]
 
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b1ecba9643db76c754fb7e75479978467dfb205e..cbcf34010d7bd2e8600915841e07f7cc47c0bceb 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -626,8 +626,8 @@ Proof.
 Qed.
 Global Instance id_free_op_r x y : IdFree y → Cancelable x → IdFree (x ⋅ y).
 Proof.
-  intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
-  eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
+  intros Hif ? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
+  apply: (id_free0_r Hif); [by eapply cmra_validN_op_r |symmetry; eauto].
 Qed.
 Global Instance id_free_op_l x y : IdFree x → Cancelable y → IdFree (x ⋅ y).
 Proof. intros. rewrite comm. apply _. Qed.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 53726ee4106de0232fa09e2fb638a23b7ab5f34c..8fc6c22b466977ec17d8fba888385ed9ad5f8fdb 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -1962,7 +1962,7 @@ Section final_limit.
     intros x. cbn.
     setoid_rewrite <- (Fep_lim_lifts_p _ _ _ _ x).
     cbn -[Fep_lim].
-    Unshelve. 2-4: eauto.
+    Unshelve. 2: eauto.
     setoid_rewrite (unfold_fold_id _ _).
     cbn. reflexivity.
   Qed.
diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v
index 70554b3a35f04a1768b6ae221b7721a7c1b77c36..e14a6cdda904586753c767229a63e409232ac6ab 100644
--- a/theories/algebra/ufrac_auth.v
+++ b/theories/algebra/ufrac_auth.v
@@ -16,11 +16,11 @@ difference:
 - We no longer have the [â—¯U{1} a] is the exclusive fragmental element (cf.
   [frac_auth_frag_validN_op_1_l]).
 *)
+From Coq Require Import QArith Qcanon.
 From iris.algebra Require Export auth frac.
 From iris.algebra Require Import ufrac.
 From iris.algebra Require Export updates local_updates.
 From iris.algebra Require Import proofmode_classes.
-From Coq Require Import QArith Qcanon.
 
 Definition ufrac_authR {SI : indexT} (A : cmraT SI) : cmraT SI :=
   authR (optionUR (prodR ufracR A)).
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index f340c8826de89b4eee83ab70c2782ad018209b75..53802c6a1fb8f35977e5ceb9c00e15eb2331afc7 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -79,11 +79,12 @@ Proof.
   apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   destruct n as [|n].
-  - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
+  - rewrite -fupd_plainly_mask_empty. iMod "H" as %?; auto.
   - iDestruct (step_fupdN_wand _ _ _ _ (|={⊤}=> ⌜φ⌝)%I with "H []") as "H'".
-    { by iApply fupd_plain_mask_empty. }
+    { unshelve iApply fupd_plain_mask_empty; apply _. }
     rewrite -step_fupdN_S_fupd.
-    iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
+    unshelve iMod (step_fupdN_plain with "H'") as "Hφ"; [apply _..|].
+    iModIntro. iNext.
     simpl; rewrite -later_laterN laterN_later.
     iNext. by iMod "Hφ".
 Qed.
@@ -94,7 +95,9 @@ Lemma step_fupdN_soundness' {SI} {Σ: gFunctors SI}  `{!invPreG Σ} φ n :
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n).
   iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
-  iApply (step_fupdN_wand with "Hiter"). by iApply (fupd_mask_weaken _ _ _).
+  iApply (step_fupdN_wand with "Hiter").
+  unshelve iApply (fupd_mask_weaken _ _ _); [apply _|].
+  done.
 Qed.
 
 
diff --git a/theories/examples/refinements/derived.v b/theories/examples/refinements/derived.v
index 931dfa3b6a8dce9d7d5f056e69e205367b5a8e0d..e8ce3e1c39e50c5f518f1cd2776bb168c220e73d 100644
--- a/theories/examples/refinements/derived.v
+++ b/theories/examples/refinements/derived.v
@@ -82,43 +82,43 @@ Section derived.
     by iApply ("H" with "P Hna").
   Qed.
 
-  Lemma TPStutterSStore (et : expr) v1 v2 K l P Q : 
+  Lemma TPStutterSStore (et : expr) v1 v2 K l P Q :
     to_val et = None
-    → {{P ∗ src (fill K (Val #())) ∗ l ↦s v2}} et {{v, Q v}} 
-    ⊢ {{l ↦s v1 ∗ src (fill K (#l <- v2)) ∗ P}} et {{v, Q v}}. 
-  Proof. 
-    iIntros (Hv) "#H !> [Hloc [Hsrc P]] Hna". 
+    → {{P ∗ src (fill K (Val #())) ∗ l ↦s v2}} et {{v, Q v}}
+    ⊢ {{l ↦s v1 ∗ src (fill K (#l <- v2)) ∗ P}} et {{v, Q v}}.
+  Proof.
+    iIntros (Hv) "#H !> [Hloc [Hsrc P]] Hna".
     iApply (rwp_weaken with "[H Hna] [P Hloc Hsrc]"); first done.
-    - instantiate (1 := (P ∗ src (fill K #()) ∗ l ↦s v2)%I). 
-      iIntros "H1". iApply ("H" with "[H1] [Hna]"); done. 
-    - iApply src_update_mono. iSplitL "Hsrc Hloc". 
-      iApply step_store. by iFrame. 
+    - instantiate (1 := (P ∗ src (fill K #()) ∗ l ↦s v2)%I).
+      iIntros "H1". iApply ("H" with "[H1] [Hna]"); done.
+    - iApply src_update_mono. iSplitL "Hsrc Hloc".
+      iApply step_store. by iFrame.
       iIntros "[H0 H1]". by iFrame.
-  Qed. 
+  Qed.
 
-  Lemma TPStutterSPure (et es es' : expr) P Q : 
+  Lemma TPStutterSPure (et es es' : expr) P Q :
     to_val et = None
     → pure_step es es'
     → {{ P ∗ src(es') }} et {{v, Q v}}
       ⊢ {{ P ∗ src(es)}} et {{v, Q v}}.
-  Proof. 
+  Proof.
     iIntros (H0 H) "#H !> [P Hsrc] Hna".
-    iApply (rwp_weaken with "[H Hna] [P Hsrc]"); first done. 
-    - instantiate (1 := (P ∗ src es')%I). iIntros "H1". 
-      by iApply ("H" with "[H1] Hna"). 
-    - iApply src_update_mono. iSplitL "Hsrc". 
-      by iApply step_pure. iIntros "?"; by iFrame. 
-  Qed.  
-
-  Lemma HoareLöb X P Q e : 
+    iApply (rwp_weaken with "[H Hna] [P Hsrc]"); first done.
+    - instantiate (1 := (P ∗ src es')%I). iIntros "H1".
+      by iApply ("H" with "[H1] Hna").
+    - iApply src_update_mono. iSplitL "Hsrc".
+      by iApply step_pure. iIntros "?"; by iFrame.
+  Qed.
+
+  Lemma HoareLöb X P Q e :
     (∀ x :X, {{P x ∗ ▷ (∀ x, {{P x}} e {{v, Q x v}})}} e {{ v, Q x v}})
-    ⊢ ∀ x, {{ P x }} e {{v, Q x v}}. 
-  Proof. 
-    iIntros "H". iApply bi.löb. 
-    iIntros "#H1" (x). 
+    ⊢ ∀ x, {{ P x }} e {{v, Q x v}}.
+  Proof.
+    iIntros "H". iApply bi.löb.
+    iIntros "#H1" (x).
     (*iIntros "H0".*)
     (*iSpecialize ("H" with x). *)
     (*iApply ("H"). iModIntro.*)
-  Abort. 
+  Abort.
 
 End derived.
diff --git a/theories/examples/refinements/memoization.v b/theories/examples/refinements/memoization.v
index 3dc4e2476deb7ab5cebbffdb56b252559aa4b4db..0acf988810ce05f71dce76cef76604d57590670d 100644
--- a/theories/examples/refinements/memoization.v
+++ b/theories/examples/refinements/memoization.v
@@ -678,8 +678,8 @@ Section fibonacci.
       rewrite bool_decide_eq_false_2; last (injection 1; lia).
       pure_exec.
     - repeat split; try solve_vals_compare_safe.
-      + rewrite /bin_op_eval //=. by replace (S (S n) - 1) with (S n: Z) by lia.
-      + rewrite /bin_op_eval //=. by replace (S (S n) - 2) with (n: Z) by lia.
+      + rewrite /bin_op_eval //=. by replace (S (S n) - 1)%Z with (S n: Z) by lia.
+      + rewrite /bin_op_eval //=. by replace (S (S n) - 2)%Z with (n: Z) by lia.
   Qed.
 
   Definition fib : val :=
@@ -742,14 +742,14 @@ Section fibonacci.
     rewrite bool_decide_eq_false_2; last (injection 1; lia).
     do 7 wp_pure _.
     (* recursion for n *)
-    wp_bind (g  _)%E. replace (S (S n) - 2) with (n: Z) by lia.
+    wp_bind (g  _)%E. replace (S (S n) - 2)%Z with (n: Z) by lia.
     src_bind (fib #n) in "Hsrc".
     iApply (rwp_wand with "[Hna Hsrc]").
     { iApply ("IH" with "[] Hsrc Hna"); first eauto. }
     iIntros (v) "[Hna H]". iDestruct "H" as (m) "(HPre & Hsrc & #Hev1)"; simpl.
     iDestruct "HPre" as %[m' [Heq1 Heq2]]. subst.
     (* recursion for (n + 1) *)
-    wp_bind (g  _)%E. replace (S (S n) - 1) with (S n: Z) by lia.
+    wp_bind (g  _)%E. replace (S (S n) - 1)%Z with (S n: Z) by lia.
     src_bind (fib _) in "Hsrc".
     iApply (rwp_wand with "[Hna Hsrc]").
     { iApply ("IH" with "[] Hsrc Hna"). eauto. }
@@ -758,7 +758,7 @@ Section fibonacci.
     iFrame. iApply (rwp_weaken with "[-Hsrc] [Hsrc]"); first done; last first.
     { iApply (steps_pure_exec with "Hsrc"). reflexivity. }
     simpl; iIntros "Hsrc"; wp_pure _.
-    replace (m + m') with ((m' + m)%nat: Z) by lia.
+    replace (m + m')%Z with ((m' + m)%nat: Z) by lia.
     iExists (m' + m)%nat; iFrame; iSplitR; auto.
     iModIntro.
     iDestruct "Hev1" as % Hev1. iDestruct "Hev2" as % Hev2. iPureIntro.
@@ -812,8 +812,8 @@ Section fibonacci.
   Proof.
     (* XXX: the iApply fails over typeclass resolution (?) if we don't do iStartProof *)
     iStartProof.
-    iApply (memoize_spec _ _ _ (λ x, ⌜ val_is_unboxed x ⌝)%I (λ x1 x2, ⌜ x1 = x2 ⌝)%I);
-      [| | iSplit; [| iSplit]].
+    unshelve iApply (memoize_spec _ _ _ (λ x, ⌜ val_is_unboxed x ⌝)%I (λ x1 x2, ⌜ x1 = x2 ⌝)%I);
+      try apply _; [| | iSplit; [| iSplit]].
     - iIntros (??) "H". iDestruct "H" as %[? [-> ->]]. eauto.
     - iIntros (??? ->). auto.
     - rewrite /eqfun. iIntros (??) "!>". iIntros (Φ) "(%&%) H".
@@ -828,8 +828,8 @@ Section fibonacci.
   Lemma fib_deep_memoized: ⊢ SEQ (mem_rec eq_heaplang fib_template) ⟨⟨ h, implements execV natRel natRel h fib ⟩⟩.
   Proof.
     iStartProof.
-    iApply (mem_rec_spec _ _ _ (λ x, ⌜ val_is_unboxed x ⌝)%I (λ x1 x2, ⌜ x1 = x2 ⌝)%I);
-      [| | iSplit; [| iSplit]].
+    unshelve iApply (mem_rec_spec _ _ _ (λ x, ⌜ val_is_unboxed x ⌝)%I (λ x1 x2, ⌜ x1 = x2 ⌝)%I);
+      try apply _; [| | iSplit; [| iSplit]].
     - iIntros (??) "H". iDestruct "H" as %[? [-> ->]]. eauto.
     - iIntros (??? ->). auto.
     - rewrite /eqfun. iIntros (??) "!>". iIntros (Φ) "(%&%) H".
@@ -1288,7 +1288,7 @@ Section levenshtein.
   { iPureIntro. do 2 f_equal. lia. }
   simpl.
   iFrame.
-  replace (1 + Z.of_nat m) with (Z.of_nat (S m)) by lia. iFrame.
+  replace (1 + Z.of_nat m)%Z with (Z.of_nat (S m)) by lia. iFrame.
   iModIntro. rewrite /eval. iIntros (vb') "#HPre". iIntros (K') "H".
   iDestruct "HPre" as (s') "#Hinv1'".
   iApply fupd_src_update.
@@ -1322,7 +1322,7 @@ Section levenshtein.
   simpl.
   rewrite -Heq2.
   do 3 src_pure _ in "H".
-  replace (1 + Z.of_nat m) with (Z.of_nat (S m)) by lia.
+  replace (1 + Z.of_nat m)%Z with (Z.of_nat (S m)) by lia.
   iApply weak_src_update_return; by iFrame.
   Qed.
 
@@ -1826,8 +1826,8 @@ Section levenshtein.
   Proof using Sync Fin.
     (* XXX: the iApply fails over typeclass resolution (?) if we don't do iStartProof *)
     iStartProof. iIntros "Hc".
-    iApply (tf_memoize_spec _ _ (λ x, ∃ (l1 l2: loc), ⌜ x = (#l1, #l2)%V ⌝)%I (λ x1 x2, ⌜ x1 = x2 ⌝)%I);
-      [| | iSplit].
+    unshelve iApply (tf_memoize_spec _ _ (λ x, ∃ (l1 l2: loc), ⌜ x = (#l1, #l2)%V ⌝)%I (λ x1 x2, ⌜ x1 = x2 ⌝)%I);
+      try apply _; [| | iSplit].
     - iIntros (??) "HPre".
       iDestruct "HPre" as (v1a v2a v1b v2b Heq1 Heq2) "(Hs1&Hs2)". subst.
       iDestruct "Hs1" as (s1) "#Hinv1".
@@ -1881,7 +1881,7 @@ Section levenshtein.
     iIntros (h) "(Hna&#Himpl)".
     wp_pures.
     rewrite /lev_template. wp_pure _. wp_pure _.
-    iApply (tf_mem_rec_spec _ _ (λ x, ∃ (l1 l2: loc), ⌜ x = (#l1, #l2)%V ⌝)%I (λ x1 x2, ⌜ x1 = x2 ⌝)%I with "[Hc2] [$Hna]"); [| | iSplit].
+    unshelve iApply (tf_mem_rec_spec _ _ (λ x, ∃ (l1 l2: loc), ⌜ x = (#l1, #l2)%V ⌝)%I (λ x1 x2, ⌜ x1 = x2 ⌝)%I with "[Hc2] [$Hna]"); try apply _; [| | iSplit].
     - iIntros (??) "HPre".
       iDestruct "HPre" as (v1a v2a v1b v2b Heq1 Heq2) "(Hs1&Hs2)". subst.
       iDestruct "Hs1" as (s1) "#Hinv1".
diff --git a/theories/examples/refinements/refinement.v b/theories/examples/refinements/refinement.v
index 9adc3df8fea11a88347b6184bf1bf954fb321297..a27e0ca1e91d33cb339741a1cd5b7be78cf245e5 100644
--- a/theories/examples/refinements/refinement.v
+++ b/theories/examples/refinements/refinement.v
@@ -787,6 +787,7 @@ Proof.
 Qed.
 
 From iris.program_logic Require Import ref_adequacy.
+From iris.heap_lang Require Import lang.
 (* Adequacy Theorem *)
 Section adequacy.
   Context {SI: indexT} `{C: Classical}  `{LI: LargeIndex SI} {Σ: gFunctors SI}.
diff --git a/theories/examples/safety/par.v b/theories/examples/safety/par.v
index 57c6ea6a9ec18ffc70690cc1b20505e9eba44cc1..43e12002d88bd1c1d85242a4e5aeaaea98acfec7 100644
--- a/theories/examples/safety/par.v
+++ b/theories/examples/safety/par.v
@@ -9,7 +9,7 @@ Definition par : val :=
   λ: "e1" "e2",
     let: "handle" := spawn "e1" in
     let: "v2" := "e2" #() in
-    let: "v1" := join "handle" in
+    let: "v1" := spawn.join "handle" in
     ("v1", "v2").
 Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
 Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
diff --git a/theories/examples/termination/adequacy.v b/theories/examples/termination/adequacy.v
index d46c9b883d8022bd490f914dd685e645184c8aea..d08a0cc5d8e228117c91998e9cfb534bd6f42e8a 100644
--- a/theories/examples/termination/adequacy.v
+++ b/theories/examples/termination/adequacy.v
@@ -11,7 +11,7 @@ Set Default Proof Using "Type".
 
 (* Adequacy Theorem *)
 Section adequacy.
-  Context {SI} `{C: Classical}  {Σ: gFunctors SI} {Hlarge: LargeIndex SI}. 
+  Context {SI} `{C: Classical}  {Σ: gFunctors SI} {Hlarge: LargeIndex SI}.
   Context `{Hpre: !heapPreG Σ} `{Hna: !na_invG Σ} `{Htc: !inG Σ (authR (ordA SI))}.
 
   Theorem heap_lang_ref_adequacy (e: expr) σ:
@@ -27,7 +27,7 @@ Section adequacy.
     eapply satisfiable_update_alloc in Hsat as [seqG_name Hsat]; last apply na_alloc.
     pose (seq := {| seqG_na_invG := _; seqG_name := seqG_name |}).
     (* allocte stuttering credits *)
-    eapply (satisfiable_at_alloc (● zero ⋅ ◯ zero)) in Hsat as [authG_name Hsat]; last first.
+    eapply (satisfiable_at_alloc (● (zero: ordA SI) ⋅ ◯ (zero: ordA SI))) in Hsat as [authG_name Hsat]; last first.
     { apply auth_both_valid; by split. }
     pose (stutter := {| sourceG_inG := _; sourceG_name := authG_name |}).
     specialize (Hobj Hheap seq stutter).
@@ -50,7 +50,7 @@ Section adequacy.
 
 End adequacy.
 
-Section adequacy_ord. 
+Section adequacy_ord.
   (* result for the ordinal step-index type *)
   Context `{C: Classical}  {Σ: gFunctors ordI}.
   Context `{Hpre: !heapPreG Σ} `{Hna: !na_invG Σ} `{Htc: !inG Σ (authR (ordA ordI))}.
@@ -62,6 +62,6 @@ Section adequacy_ord.
   Proof using C Σ Hpre Hna Htc.
     apply heap_lang_ref_adequacy.
   Qed.
-  Print Assumptions heap_lang_ref_adequacy_ord. 
+  Print Assumptions heap_lang_ref_adequacy_ord.
 
 End adequacy_ord.
diff --git a/theories/examples/termination/eventloop.v b/theories/examples/termination/eventloop.v
index de992cf02a315d01d7ef9853d33d0689441c0a18..be19d594d7848d50d0c1ec1e115b9d54014e26e2 100644
--- a/theories/examples/termination/eventloop.v
+++ b/theories/examples/termination/eventloop.v
@@ -185,17 +185,17 @@ Section open_example.
     WP e;; (for: #n do e)%V [{v, φ v}] ⊢ WP (for: #(S n) do e)%V [{ v, φ v }].
   Proof.
     rewrite /for_loop; iIntros "H". wp_pures.
-    by replace (S n - 1) with (n: Z) by lia.
+    by replace (S n - 1)%Z with (n: Z) by lia.
   Qed.
 
   Lemma example_spec `{FiniteBoundedExistential SI}:
-    queue N q ∗ $ (omul one) ∗ SEQ external_code #() [{ v, ∃ n: nat, ⌜v = #n⌝ }] ∗ (□ ∀ s: string, SEQ print s [{ _, True }]) ⊢
+    queue N q ∗ $ (omul (one: ordA SI)) ∗ SEQ external_code #() [{ v, ∃ n: nat, ⌜v = #n⌝ }] ∗ (□ ∀ s: string, SEQ print s [{ _, True }]) ⊢
     SEQ example [{ _, True }].
   Proof.
     iIntros "(#Q & Hc & Hwp & #Hprint) Hna". rewrite /example.
     wp_bind (external_code _). iMod ("Hwp" with "Hna") as "_".
     iIntros (v) "[Hna Hn] !>". iDestruct "Hn" as (n) "->".
-    do 2 wp_pure _. iApply (tc_weaken (omul one) (natmul (n * 2)%nat one)); auto; first apply (ord_stepindex.limit_upper_bound (λ n, natmul n one)).
+    do 2 wp_pure _. iApply (tc_weaken (omul (one: ordA SI)) (natmul (n * 2)%nat (one: ordA SI))); auto; first apply (ord_stepindex.limit_upper_bound (λ n, natmul n one)).
     iFrame "Hc". iIntros "Hc". iApply for_val.
     iInduction n as [|n] "IH".
     - iMod (for_zero) as "_"; iFrame; auto.
diff --git a/theories/examples/termination/logrel.v b/theories/examples/termination/logrel.v
index 2452064b95ba3ad92547554646946ee78a83d784..261fa3cb791f3464d9b5dfe43f2c9f64d49000d3 100644
--- a/theories/examples/termination/logrel.v
+++ b/theories/examples/termination/logrel.v
@@ -203,7 +203,7 @@ Section semantic_model.
       wp_pure _; first naive_solver. wp_pures. by iFrame.
     - rewrite tc_split. iDestruct "Hc" as "[Hα Hc]".
       rewrite /iter. wp_pures. wp_pure _; first naive_solver.
-      wp_pures. replace (S n - 1) with (n: Z) by lia.
+      wp_pures. replace (S n - 1)%Z with (n: Z) by lia.
       iApply ("IH" with "[Hα Hv] Hc Hna"). iApply ("H2" with "Hα Hv").
   Qed.
 
@@ -368,7 +368,7 @@ Section semantic_model.
   Proof.
     iExists ord_stepindex.zero. iIntros "_".
     iIntros (θ) "HΓ". rewrite /env_ltyped.
-    iPoseProof (big_sepM_lookup _ _ x A with "HΓ") as "Hx"; first eapply lookup_insert.
+    unshelve iPoseProof (big_sepM_lookup _ _ x A with "HΓ") as "Hx"; [apply _|eapply lookup_insert|].
     simpl; iDestruct "Hx" as (v) "(-> & HA)".
     by iApply seq_value.
   Qed.
@@ -603,7 +603,7 @@ Section semantic_model.
   Proof.
     iExists ord_stepindex.zero. iIntros "_".
     iIntros (δ) "%". iIntros (θ) "HΓ". rewrite /env_lptyped /env_ltyped big_opM_fmap.
-    iPoseProof (big_sepM_lookup _ _ x T with "HΓ") as "Hx"; first eapply lookup_insert.
+    unshelve iPoseProof (big_sepM_lookup _ _ x T with "HΓ") as "Hx"; [apply _|eapply lookup_insert|].
     simpl; iDestruct "Hx" as (v) "(-> & HA)".
     by iApply seq_value.
   Qed.
@@ -889,7 +889,7 @@ Section adequacy.
 
 End adequacy.
 
-Section ordinals. 
+Section ordinals.
   Context `{C: Classical}  {Σ: gFunctors ordI}.
   Context `{Hpre: !heapPreG Σ} `{Hna: !na_invG Σ} `{Htc: !inG Σ (authR (ordA ordI))}.
 
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 40d499bbe9764fa688d7a797445a864f20ea4b7c..81e9f85fcf86dbdbcd3534c7bf75400cf00cee9c 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -321,7 +321,7 @@ Qed.
 
 (** Heap *)
 Lemma wp_allocN s E v n :
-  0 < n →
+  (0 < n)%Z →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
          [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
@@ -337,7 +337,7 @@ Proof.
   - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
 Lemma swp_allocN k s E v n :
-  0 < n →
+  (0 < n)%Z →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) at k @ s; E
   {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
          [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
@@ -1001,7 +1001,7 @@ Qed.
 
 (** Heap *)
 Lemma rswp_allocN k s E v n :
-  0 < n →
+  (0 < n)%Z →
   ⟨⟨⟨ True ⟩⟩⟩ AllocN (Val $ LitV $ LitInt $ n) (Val v) at k @ s; E
   ⟨⟨⟨ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
          [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ ⟩⟩⟩.
@@ -1207,7 +1207,7 @@ Qed.
 
 (** Heap *)
 Lemma rwp_allocN s E v n :
-  0 < n →
+  (0 < n)%Z →
   ⟨⟨⟨ True ⟩⟩⟩ AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   ⟨⟨⟨ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
          [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ ⟩⟩⟩.
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 9df37184bacf13d0a4d26fa7f33a4967e6d467ef..5cbe982ee30be5ceb226dc5d3495f055699e9e36 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -93,10 +93,10 @@ Proof.
 Qed.
 
 Lemma heap_closed_alloc σ l n w :
-  0 < n →
+  (0 < n)%Z →
   is_closed_val w →
   map_Forall (λ _ v, is_closed_val v) (heap σ) →
-  (∀ i : Z, 0 ≤ i → i < n → heap σ !! (l +ₗ i) = None) →
+  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
   map_Forall (λ _ v, is_closed_val v)
              (heap_array l (replicate (Z.to_nat n) w) ∪ heap σ).
 Proof.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 100a4b3218558267bce41b69cb00d11c686a9e9e..4708be6b7803e57ce42c412a4939eb32565cfe9b 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -12,11 +12,12 @@ Lemma lstep_fupd_soundness {SI} {Σ: gFunctors SI} `{TransfiniteIndex SI} `{!inv
 Proof.
   intros Hiter. assert ((True ⊢ ⧍^n ⌜φ⌝ : iProp Σ)%I → φ) as Hlater;
                   last (apply Hlater).
-  { intros H1. 
-    eapply pure_soundness, uPred_primitive.big_laterN_soundness, H1. 
+  { intros H1.
+    eapply pure_soundness, uPred_primitive.big_laterN_soundness, H1.
   }
   apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
-  iPoseProof (Hiter Hinv) as "H". by iApply lstep_fupdN_plain.
+  iPoseProof (Hiter Hinv) as "H". unshelve iApply lstep_fupdN_plain; [apply _..|].
+  done.
 Qed.
 
 Section adequacy.
@@ -31,7 +32,7 @@ Implicit Types Φs : list (val Λ → iProp Σ).
 Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ fork_post }})%I.
 
 Existing Instance elim_eventuallyN.
-Existing Instance elim_gstep. 
+Existing Instance elim_gstep.
 Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
   state_interp σ1 (κ ++ κs) m -∗ WP e1 @ s; ⊤ {{ Φ }} -∗ >={⊤}=={⊤}=>
@@ -39,10 +40,10 @@ Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
   rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
-  iMod ("H" $! σ1 with "Hσ") as "H". iMod "H". 
-  iDestruct "H" as (n) "H". 
-  iApply (gstepN_gstep _ _ _ (S n)). iModIntro. 
-  replace (S n) with (n + 1) by lia. iApply eventuallyN_compose. iMod "H". 
+  iMod ("H" $! σ1 with "Hσ") as "H". iMod "H".
+  iDestruct "H" as (n) "H".
+  iApply (gstepN_gstep _ _ _ (S n)). iModIntro.
+  replace (S n) with (n + 1) by lia. iApply eventuallyN_compose. iMod "H".
   iMod "H" as "[% H]". iMod ("H" $! e2 σ2 efs with "[//]") as "H".
   by iIntros "!> !> !> !>".
 Qed.
@@ -67,19 +68,19 @@ Proof.
 Qed.
 
 Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
-  nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
+  language.nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   state_interp σ1 (κs ++ κs') (length t1) -∗ WP e1 @ s; ⊤ {{ Φ }} -∗ wptp s t1
   -∗ (>={⊤}=={⊤}=>^n
   (∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗
     state_interp σ2 κs' (pred (length t2)) ∗
-    WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2')). 
+    WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2')).
 Proof.
   revert e1 t1 κs κs' t2 σ1 σ2; simpl.
   induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
   { inversion_clear 1; iIntros "???"; iExists e1, t1; iFrame; eauto 10. }
   iIntros (Hsteps) "Hσ He Ht". inversion_clear Hsteps as [|?? [t1' σ1']].
   rewrite -(assoc_L (++)).
-  iPoseProof (wptp_step with "Hσ He Ht")  as (e1' t1'' ?) ">(Hσ & He & Ht)"; first eauto. 
+  iPoseProof (wptp_step with "Hσ He Ht")  as (e1' t1'' ?) ">(Hσ & He & Ht)"; first eauto.
   simplify_eq. by iApply (IH with "Hσ He Ht").
 Qed.
 
@@ -91,10 +92,10 @@ Proof.
   destruct (to_val e) as [v|] eqn:?; first by eauto.
   iSpecialize ("H" $! σ [] κs with "Hσ").
   iAssert (|={⊤,∅}=> ⧍ ⌜reducible e σ⌝)%I with "[H]" as "H".
-  { iMod "H". iMod (eventually_plain with "[H]") as "H"; last by iModIntro. apply _.
-    iMod "H" as (n) "H". iModIntro. iExists (S n). replace (S n) with (n + 1)by lia. iApply eventuallyN_compose. 
-    iMod "H". by iMod "H" as "[$ _]". } 
-  iMod (fupd_plain_mask with "H") as "H"; eauto.
+  { iMod "H". unshelve iMod (eventually_plain with "[H]") as "H"; last (by iModIntro); [apply _..|].
+    iMod "H" as (n) "H". iModIntro. iExists (S n). replace (S n) with (n + 1)by lia. iApply eventuallyN_compose.
+    iMod "H". by iMod "H" as "[$ _]". }
+  unshelve iMod (fupd_plain_mask with "H") as "H"; [apply _..|]; eauto.
   iModIntro. iMod "H" as "%". by iRight.
 Qed.
 
@@ -109,14 +110,14 @@ Qed.
 
 Lemma big_later_eventually P E: ⧍ P -∗ <E> P.
 Proof.
-  iDestruct 1 as (n) "H". iExists n. 
-  iModIntro. iInduction n as [ | n] "IH"; simpl; eauto. 
-  iModIntro. iNext. iModIntro. by iApply "IH". 
+  iDestruct 1 as (n) "H". iExists n.
+  iModIntro. iInduction n as [ | n] "IH"; simpl; eauto.
+  iModIntro. iNext. iModIntro. by iApply "IH".
 Qed.
 
-Existing Instance elim_gstep_N. 
+Existing Instance elim_gstep_N.
 Lemma wptp_strong_adequacy Φ κs' s n e1 t1 κs e2 t2 σ1 σ2 :
-  nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
+  language.nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   state_interp σ1 (κs ++ κs') (length t1) -∗
   WP e1 @ s; ⊤ {{ Φ }} -∗
   wptp s t1 -∗ >={⊤}=={⊤}=>^(S n) ∃ e2 t2',
@@ -164,7 +165,7 @@ Proof.
 Qed.
 End adequacy.
 
-Existing Instance elim_gstep_N. 
+Existing Instance elim_gstep_N.
 (** Iris's generic adequacy result *)
 Theorem wp_strong_adequacy {SI} `{TransfiniteIndex SI} (Σ: gFunctors SI) Λ `{!invPreG Σ} e1 σ1 n κs t2 σ2 φ :
   (∀ `{Hinv : !invG Σ},
@@ -192,7 +193,7 @@ Theorem wp_strong_adequacy {SI} `{TransfiniteIndex SI} (Σ: gFunctors SI) Λ `{!
          one can use [fupd_intro_mask'] or [fupd_mask_weaken] to introduce the
          fancy update. *)
          |={⊤,∅}=> ⌜ φ ⌝))%I) →
-  nsteps n ([e1], σ1) κs (t2, σ2) →
+  language.nsteps n ([e1], σ1) κs (t2, σ2) →
   (* Then we can conclude [φ] at the meta-level. *)
   φ.
 Proof.
@@ -200,12 +201,12 @@ Proof.
   eapply (@lstep_fupd_soundness _ Σ _ _ _ (S (S n) + 1))=> Hinv.
   rewrite Nat_iter_add Nat_iter_S.
   iMod Hwp as (s stateI Φ fork_post) "(Hσ & Hwp & Hφ)".
-  iApply lstep_intro. iModIntro. 
+  iApply lstep_intro. iModIntro.
   iPoseProof (@wptp_strong_adequacy _ _ _ (IrisG _ _ _ Hinv stateI fork_post) _ []
   with "[Hσ] Hwp") as "Hpost". 1-3:eauto. by rewrite right_id_L. iSpecialize ("Hpost" with "[$]").
   iMod "Hpost". iDestruct "Hpost" as (e2 t2' ->) "(? & ? & ? & ?)".
-  iApply lstep_intro. 
-  iApply fupd_plain_mask_empty.
+  iApply lstep_intro.
+  unshelve iApply fupd_plain_mask_empty; [apply _..|].
   iMod ("Hφ" with "[% //] [$] [$] [$] [$]"). done.
 Qed.
 
diff --git a/theories/program_logic/refinement/ref_source.v b/theories/program_logic/refinement/ref_source.v
index e269ea4370de3765ea8e37e728fa008e9ddf9c92..a85a6828fb7bd254abab7338b00672866f8f6d09 100644
--- a/theories/program_logic/refinement/ref_source.v
+++ b/theories/program_logic/refinement/ref_source.v
@@ -280,7 +280,7 @@ Section ord_auth_source.
     srcF ordA (n ⊕ m) ⊣⊢ srcF ordA n ∗ srcF ordA m.
   Proof. apply srcF_split. Qed.
 
-  Definition one := succ zero.
+  Definition one : ordA := succ (zero).
   Lemma ord_srcF_succ `{!auth_sourceG Σ ordA} (n: Ord):
     srcF ordA (succ n) ⊣⊢ srcF ordA one ∗ srcF ordA n.
   Proof.
@@ -291,6 +291,8 @@ Section ord_auth_source.
 
 End ord_auth_source.
 
+Global Arguments one {_}.
+
 Inductive lex {X Y} (R: X → X → Prop) (S: Y → Y → Prop) : (X * Y) → (X * Y) -> Prop :=
 | lex_left x x' y y': R x x' → lex R S (x, y) (x', y')
 | lex_right x y y': S y y' → lex R S (x, y) (x, y').
diff --git a/theories/program_logic/refinement/tc_weakestpre.v b/theories/program_logic/refinement/tc_weakestpre.v
index a5f00b1a4b2b9a3ef940c65a866bc4f507e12926..782fe270be3cc262929c40d84fbef50264563e40 100644
--- a/theories/program_logic/refinement/tc_weakestpre.v
+++ b/theories/program_logic/refinement/tc_weakestpre.v
@@ -14,7 +14,7 @@ Global Program Instance tcwp {SI} {Σ: gFunctors SI} `{!tcG Σ} `{!ref_irisG Λ
 Section lemmas.
   Context {SI} {Σ: gFunctors SI} {Λ} `{!ref_irisG Λ Σ} `{!tcG Σ}.
 
-  Definition one := (succ zero).
+  Definition one : ordA SI := (succ zero).
 
   Lemma tc_split α β: $ (α ⊕ β) ≡ ($α ∗ $β)%I.
   Proof.
@@ -58,7 +58,7 @@ Section lemmas.
     iIntros "H".
     iMod (@own_unit _ _ _ sourceG_inG sourceG_name) as "Hz".
     replace (ε: @authR SI (auth_sourceUR SI (ordA SI)))
-      with (â—¯ zero: @authR SI (auth_sourceUR SI (ordA SI))) by reflexivity.
+      with ((â—¯ (zero: ordA SI))) by reflexivity.
     by iSpecialize ("H" with "Hz").
   Qed.
 
@@ -68,7 +68,7 @@ Section lemmas.
   Global Instance zero_persistent : Persistent ($ zero).
   Proof.
     apply own_core_persistent, auth_frag_core_id.
-    replace zero with (core zero) by reflexivity.
+    replace zero with (core (zero: ordA SI)) by reflexivity.
     apply cmra_core_core_id.
   Qed.
 
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index f7a523d327814b87040ac390cb4ba7341846e29b..f0d5d9ed2ac9619330570498c6ae6a9a4658ee19 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -32,7 +32,7 @@ Section eventually.
     - simpl. iSpecialize ("IH" with "H").
       iMod "IH".
       iPoseProof (fupd_trans with "IH") as "IH".
-      iPoseProof (fupd_plain_later with "IH") as "IH".
+      unshelve iPoseProof (fupd_plain_later with "IH") as "IH"; first apply _.
       iMod "IH". iModIntro.
       iNext. by iApply except_0_later.
   Qed.
@@ -51,11 +51,12 @@ Section eventually.
     Plain P → ((>={⊤}=={⊤}=> P) ⊢ |={⊤}=> ⧍ P)%I.
   Proof.
     iIntros (HP) "H".
-    iApply (fupd_plain_mask _ ∅). iMod "H".
-    iApply eventually_plain.
+    unshelve iApply (fupd_plain_mask _ ∅); first apply _.
+    iMod "H". iApply eventually_plain.
     iApply eventually_fupd_right.
     iMod "H" as (n) "H". iApply (eventuallyN_eventually (n)).  iMod "H".
-    by iApply (fupd_plain_mask _ ⊤).
+    unshelve iApply (fupd_plain_mask _ ⊤); [apply _|].
+    done.
   Qed.
 
   Lemma lstep_fupdN_plain `{BP: BiPlainly SI PROP} `{@BiFUpdPlainly SI PROP FU BP} (P : PROP) n: