diff --git a/coq-lifetime-logic.opam b/coq-lifetime-logic.opam
index 9c4895ac2b91fe4f711dc75173f08ea59eb9880a..992861c025324d16b60016d1e810f8406675f10c 100644
--- a/coq-lifetime-logic.opam
+++ b/coq-lifetime-logic.opam
@@ -12,7 +12,7 @@ The lifetime logic extends Iris with a notion of "borrowing".
"""
depends: [
- "coq-iris" { (= "dev.2025-03-25.0.79d33e24") | (= "dev") }
+ "coq-iris" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
]
build: ["./make-package" "lifetime" "-j%{jobs}%"]
diff --git a/lambda-rust/lang/heap.v b/lambda-rust/lang/heap.v
index 030e72f27a21dd2f5e279b52b617dfadeb0a331e..47bfbaa96ba9b766f50e8668b9c8e36771368a23 100644
--- a/lambda-rust/lang/heap.v
+++ b/lambda-rust/lang/heap.v
@@ -396,7 +396,7 @@ Section heap.
assert (([^op list] k↦y ∈ vl,
{[l +â‚— (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
{ move: (Hvalid l). rewrite lookup_op lookup_singleton.
- by move=> /(cmra_discrete_valid_iff 0) /exclusiveN_Some_l. }
+ by move=> /(cmra_discrete_valid_iff 0áµ¢) /exclusiveN_Some_l. }
rewrite -insert_singleton_op //. etrans.
{ apply (delete_local_update _ _ l (1%Qp, Cinr 0%nat, to_agree v)).
by rewrite lookup_insert. }
diff --git a/lambda-rust/typing/lib/rc/rc.v b/lambda-rust/typing/lib/rc/rc.v
index 16fdab171b1d5524efddaa4a1f4aba75f0a7b428..ffad75290835972a7a1d7bdceca11b3959ef5df7 100644
--- a/lambda-rust/typing/lib/rc/rc.v
+++ b/lambda-rust/typing/lib/rc/rc.v
@@ -291,7 +291,8 @@ Section code.
* iExists _. iFrame "Hl2". destruct weak.
-- iLeft. iSplit; first done. rewrite Hincls. iFrame "Hl†".
iMod (own_update_2 with "Hst Htok") as "Hst".
- { apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
+ { apply auth_update_dealloc.
+ rewrite -{1}(right_id ((None, 0%nat) : prodUR _ _) _ (_, _)).
apply cancel_local_update_unit, _. }
rewrite -[in (1).[ν]%I]Hqq' -[(|={lft_userE,⊤}=>_)%I]fupd_trans.
iApply step_fupd_mask_mono;
@@ -353,7 +354,8 @@ Section code.
-- iLeft. iFrame. iSplitR; first done.
iApply ("Hclose" with "[>- $Hna]"). iExists (None, 0%nat).
iMod (own_update_2 with "Hst Htok") as "$"; last done.
- apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
+ apply auth_update_dealloc.
+ rewrite -{1}(right_id ((None, 0%nat) : prodUR _ _) _ (_, _)).
apply cancel_local_update_unit, _.
-- iRight. iSplitR; first by auto with lia. iIntros "!> Hl†Hl2 Hvl".
iApply ("Hclose" with "[>- $Hna]"). iExists (None, S weak).
@@ -372,7 +374,7 @@ Section code.
iFrame. iExists _. iFrame. auto with iFrame.
* iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc.
- rewrite pair_op Cinl_op Some_op -{1}(left_id 0%nat _ weak) pair_op.
+ rewrite pair_op Cinl_op Some_op -{1}(left_id (0%nat : natUR) _ weak) pair_op.
apply (cancel_local_update_unit _ (_, _)). }
iApply "Hclose". iFrame "Hst Hl2 Hl†Hna Hν†". iExists (q+q'')%Qp. iFrame.
iSplitL; first last.
diff --git a/lambda-rust/typing/type.v b/lambda-rust/typing/type.v
index f2ae8ad1bb8efc05c04d0820c08604eb9f3b1356..ed17efb099d7bb0e0b8d6cb97e61b06248b103c1 100644
--- a/lambda-rust/typing/type.v
+++ b/lambda-rust/typing/type.v
@@ -295,8 +295,8 @@ Section type_dist2.
Proof. intros EQ. split; intros; try apply dist_dist_later; apply EQ. Qed.
Lemma type_dist2_dist_later n ty1 ty2 : type_dist2 n ty1 ty2 → dist_later n ty1 ty2.
Proof.
- intros EQ. eapply dist_later_fin_iff. destruct n; first done.
- split; intros; try apply EQ; try si_solver.
+ intros EQ. dist_later_fin_intro.
+ split; intros; try apply EQ; eauto using SIdx.lt_succ_diag_r.
apply dist_S, EQ.
Qed.
Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2 → type_dist2_later n ty1 ty2.
@@ -310,7 +310,7 @@ Section type_dist2.
Proof. intros ?? EQ. apply EQ. Qed.
Lemma ty_own_type_dist n:
Proper (type_dist2 (S n) ==> eq ==> eq ==> dist n) ty_own.
- Proof. intros ?? EQ ??-> ??->. apply EQ. si_solver. Qed.
+ Proof. intros ?? EQ ??-> ??->. apply EQ, SIdx.lt_succ_diag_r. Qed.
Lemma ty_shr_type_dist n :
Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
@@ -376,9 +376,7 @@ End type_contractive.
(* Tactic automation. *)
Ltac f_type_equiv :=
first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
- match goal with | |- @dist_later ?A _ ?n ?x ?y =>
- eapply dist_later_fin_iff; destruct n as [|n]; [exact I|change (@dist A _ n x y)]
- end ].
+ dist_later_fin_intro ].
Ltac solve_type_proper :=
constructor;
solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv).
@@ -478,7 +476,7 @@ Section type.
Global Instance copy_equiv : Proper (equiv ==> impl) Copy.
Proof.
- intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1. split.
+ intros ty1 ty2 [EQsz EQown EQshr] Hty1. split.
- intros. rewrite -EQown. apply _.
- intros *. rewrite -EQsz -EQshr. setoid_rewrite <-EQown.
apply copy_shr_acc.
@@ -504,13 +502,13 @@ Section type.
(** Send and Sync types *)
Global Instance send_equiv : Proper (equiv ==> impl) Send.
Proof.
- intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
+ intros ty1 ty2 [EQsz EQown EQshr] Hty1.
rewrite /Send=>???. rewrite -!EQown. auto.
Qed.
Global Instance sync_equiv : Proper (equiv ==> impl) Sync.
Proof.
- intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
+ intros ty1 ty2 [EQsz EQown EQshr] Hty1.
rewrite /Send=>????. rewrite -!EQshr. auto.
Qed.
@@ -552,7 +550,7 @@ Section iprop_subtyping.
Global Instance type_incl_ne : NonExpansive2 type_incl.
Proof.
- intros n ?? [EQsz1%leibniz_equiv EQown1 EQshr1] ?? [EQsz2%leibniz_equiv EQown2 EQshr2].
+ intros n ?? [EQsz1 EQown1 EQshr1] ?? [EQsz2 EQown2 EQshr2].
rewrite /type_incl. repeat ((by auto) || f_equiv).
Qed.
Global Instance type_incl_proper :
@@ -576,7 +574,7 @@ Section iprop_subtyping.
Global Instance type_equal_ne : NonExpansive2 type_equal.
Proof.
- intros n ?? [EQsz1%leibniz_equiv EQown1 EQshr1] ?? [EQsz2%leibniz_equiv EQown2 EQshr2].
+ intros n ?? [EQsz1 EQown1 EQshr1] ?? [EQsz2 EQown2 EQshr2].
rewrite /type_equal. repeat ((by auto) || f_equiv).
Qed.
Global Instance type_equal_proper :